Agda-2.3.0.1: 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 aSource
Create an open term which is closed.
getOpen :: Raise a => Open a -> TCM aSource
Extract the value from an open term. Must be done in an extension of the context in which the term was created.
tryOpen :: Raise a => Open a -> TCM (Maybe a)Source