ModuleAgda-2.7.0.1Haskell2010

Agda.TypeChecking.Monad.Open

4 values

PackageAgda-2.7.0.1
Exports4
LanguageHaskell2010
LicenceMIT
SourceOpen.hs

valuemakeOpen :: (ReadTCState m, MonadTCEnv m) => a -> m (Open a)

Create an open term in the current context.

valuegetOpen :: (TermSubst 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.

valuetryGetOpen

:: (TermSubst a, ReadTCState m, MonadTCEnv m)
=> Substitution -> a -> Maybe a
-> Open a
-> m (Maybe a)

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.

valueisClosed :: Open a -> Bool

An Open is closed if it has checkpoint 0.