Agda-2.4.2.3: A dependently typed functional programming language and proof assistant
Agda.TypeChecking.Monad.Open
Synopsis
makeOpen :: a -> TCM (Open a) Source
Create an open term in the current context.
makeClosed :: a -> Open a Source
Create an open term which is closed.
getOpen :: Subst a => Open a -> TCM a Source
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) Source
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