Agda-2.6.1.3: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Monad.Open

Synopsis

Documentation

makeOpen :: MonadTCEnv m => a -> m (Open a) Source #

Create an open term in the current context.

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

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) Source #

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 Source #

An Open is closed if it has checkpoint 0.