Agda-2.4.2.3: A dependently typed functional programming language and proof assistant
Agda.TypeChecking.Monad.Open
Synopsis
makeOpen :: a -> TCM (Open a)
Create an open term in the current context.
makeClosed :: a -> Open a
Create an open term which is closed.
getOpen :: Subst a => Open a -> TCM a
Extract the value from an open term. Must be done in an extension of the context in which the term was created.
tryOpen :: Subst a => Open a -> TCM (Maybe a)
Try to use an Open the current context. Returns Nothing if current context is not an extension of the context in which the Open was created.
Open
Nothing