| Safe Haskell | None |
|---|
Agda.TypeChecking.Monad.Env
- currentModule :: TCM ModuleName
- withCurrentModule :: ModuleName -> TCM a -> TCM a
- getAnonymousVariables :: ModuleName -> TCM Nat
- withAnonymousModule :: ModuleName -> Nat -> TCM a -> TCM a
- withEnv :: TCEnv -> TCM a -> TCM a
- getEnv :: TCM TCEnv
- withIncreasedModuleNestingLevel :: TCM a -> TCM a
Documentation
currentModule :: TCM ModuleNameSource
Get the name of the current module, if any.
withCurrentModule :: ModuleName -> TCM a -> TCM aSource
Set the name of the current module.
getAnonymousVariables :: ModuleName -> TCM NatSource
Get the number of variables bound by anonymous modules.
withAnonymousModule :: ModuleName -> Nat -> TCM a -> TCM aSource
Add variables bound by an anonymous module.
withIncreasedModuleNestingLevel :: TCM a -> TCM aSource
Increases the module nesting level by one in the given computation.