module VerifiedCompilation.Purity where
open import Untyped using (_⊢; case; builtin; _·_; force; `; ƛ; delay; con; constr; error) open import Relation.Nullary using (Dec; yes; no; ¬_)
data UPure (X : Set) : (X ⊢) → Set where FIXME : (t : X ⊢) → UPure X t isUPure? : {X : Set} → (t : X ⊢) → Dec (UPure X t) isUPure? t = yes (FIXME t)