| Safe Haskell | Safe-Infered |
|---|
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
- leaveTopLevel :: TCM a -> TCM a
- onTopLevel :: TCM Bool
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.
leaveTopLevel :: TCM a -> TCM aSource
Leave the top level to type check local things.