Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Monad.Open

Synopsis

- makeOpen :: a -> TCM (Open a)
- getOpen :: (Subst Term a, MonadTCEnv m) => Open a -> m a
- tryGetOpen :: (Subst Term a, MonadTCEnv m) => Open a -> m (Maybe a)
- isClosed :: Open a -> Bool

# Documentation

makeOpen :: a -> TCM (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.