Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.TypeChecking.Monad.Env

Synopsis

- 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 ModuleName

Get the name of the current module, if any.

withCurrentModule :: ModuleName -> TCM a -> TCM a

Set the name of the current module.

getAnonymousVariables :: ModuleName -> TCM Nat

Get the number of variables bound by anonymous modules.

withAnonymousModule :: ModuleName -> Nat -> TCM a -> TCM a

Add variables bound by an anonymous module.

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

Set the current environment to the given

getEnv :: TCM TCEnv

Get the current environment

withIncreasedModuleNestingLevel :: TCM a -> TCM a

Increases the module nesting level by one in the given computation.