Agda.TypeChecking.Monad.Open

Documentation

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.