Agda- A dependently typed functional programming language and proof assistant

Safe HaskellSafe-Infered




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.

withEnv :: TCEnv -> TCM a -> TCM aSource

Set the current environment to the given

getEnv :: TCM TCEnvSource

Get the current environmnet

leaveTopLevel :: TCM a -> TCM aSource

Leave the top level to type check local things.