Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.TypeChecking.Monad.Env
Synopsis
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.
withEnv :: MonadTCM tcm => TCEnv -> tcm a -> tcm aSource
Set the current environment to the given
getEnv :: MonadTCM tcm => tcm TCEnvSource
Get the current environmnet
Produced by Haddock version 2.4.2