Agda-2.6.2.2.20230105: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Monad.Open

Synopsis

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.