| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Monad.Open
Synopsis
- makeOpen :: MonadTCEnv m => a -> m (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 :: MonadTCEnv m => a -> m (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.