| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Syntax.Scope.State
Description
General functions for stateful manipulation of the scope.
Synopsis
- type ScopeM = TCM
- getCurrentModule :: ReadTCState m => m ModuleName
- setCurrentModule :: MonadTCState m => ModuleName -> m ()
- withCurrentModule :: (ReadTCState m, MonadTCState m) => ModuleName -> m a -> m a
- withCurrentModule' :: (MonadTrans t, Monad (t ScopeM)) => ModuleName -> t ScopeM a -> t ScopeM a
The scope checking monad
To simplify interaction between scope checking and type checking (in particular when chasing imports), we use the same monad.
Current module
getCurrentModule :: ReadTCState m => m ModuleName Source #
setCurrentModule :: MonadTCState m => ModuleName -> m () Source #
withCurrentModule :: (ReadTCState m, MonadTCState m) => ModuleName -> m a -> m a Source #
withCurrentModule' :: (MonadTrans t, Monad (t ScopeM)) => ModuleName -> t ScopeM a -> t ScopeM a Source #