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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Monad.Open

Synopsis

- makeOpen :: (ReadTCState m, MonadTCEnv m) => a -> m (Open a)
- getOpen :: (TermSubst a, MonadTCEnv m) => Open a -> m a
- tryGetOpen :: (TermSubst a, ReadTCState m, MonadTCEnv m) => (Substitution -> a -> Maybe a) -> Open a -> m (Maybe a)
- isClosed :: Open a -> Bool

# Documentation

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

Create an open term in the current context.

getOpen :: (TermSubst 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 :: (TermSubst a, ReadTCState m, MonadTCEnv m) => (Substitution -> a -> Maybe a) -> Open a -> m (Maybe a) Source #

Extract the value from an open term. If the checkpoint is no longer in scope use the provided function to pull the object to the most recent common checkpoint. The function is given the substitution from the common ancestor to the checkpoint of the thing.

isClosed :: Open a -> Bool Source #

An `Open` is closed if it has checkpoint 0.