| 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)
- tryGetOpenRew :: MonadTCEnv m => (Substitution -> m RewriteRule) -> Open RewriteRule -> m RewriteRule
- 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.
Arguments
| :: MonadTCEnv m | |
| => (Substitution -> m RewriteRule) | Action to take if the substitution fails |
| -> Open RewriteRule | The rewrite rule we are trying to open |
| -> m RewriteRule |
Try to extract the value from an open local rewrite rule. The checkpoint at which it was created must be in scope.