ModuleAgda-2.8.0.2Haskell2010

Agda.TypeChecking.Monad.Open

Synopsis

value makeOpen
value getOpen
value tryGetOpen
value isClosed

PackageAgda-2.8.0.2
Exports4
LanguageHaskell2010
LicenceMIT
SourceOpen.hs

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

Source#

Create an open term in the current context.

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

valuetryGetOpen

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

valueisClosed :: Open a -> Bool

Source#

An Open is closed if it has checkpoint 0.