Agda.TypeChecking.Monad.Open

Documentation

makeOpen :: a -> TCM (Open a)

Create an open term in the current context.

getOpen :: (Subst Term a, MonadTCEnv m) => Open a -> m a

Extract the value from an open term. The checkpoint at which it was created must be in scope.

tryGetOpen :: (Subst Term a, MonadTCEnv m) => Open a -> m (Maybe a)

Extract the value from an open term. Returns Nothing if the checkpoint at which it was created is not in scope.

isClosed :: Open a -> Bool

An Open is closed if it has checkpoint 0.