{-# OPTIONS --cubical-compatible #-}

module Terra.Tactics where
open import Terra.Data.Level
open import Terra.Data.Decision

private
  variable
    ℓ : Level

give : (T : Set ℓ) -> {{T}} -> T
give T {{v}} = v

unwrap : {T : Set ℓ} -> {{dec : Decision T}} -> {p : ⌊ dec ⌋} -> T
unwrap {p = p} = ⌊⌋-elim p