- currentModule :: MonadTCM tcm => tcm ModuleName
- withCurrentModule :: MonadTCM tcm => ModuleName -> tcm a -> tcm a
- getAnonymousVariables :: MonadTCM tcm => ModuleName -> tcm Nat
- withAnonymousModule :: MonadTCM tcm => ModuleName -> Nat -> tcm a -> tcm a
- withEnv :: MonadTCM tcm => TCEnv -> tcm a -> tcm a
- getEnv :: MonadTCM tcm => tcm TCEnv
Documentation
currentModule :: MonadTCM tcm => tcm ModuleNameSource
Get the name of the current module, if any.
withCurrentModule :: MonadTCM tcm => ModuleName -> tcm a -> tcm aSource
Set the name of the current module.
getAnonymousVariables :: MonadTCM tcm => ModuleName -> tcm NatSource
Get the number of variables bound by anonymous modules.
withAnonymousModule :: MonadTCM tcm => ModuleName -> Nat -> tcm a -> tcm aSource
Add variables bound by an anonymous module.