| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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

Get the name of the current module, if any.

withCurrentModule :: MonadTCM tcm => ModuleName -> tcm a -> tcm a | Source

Set the name of the current module.

getAnonymousVariables :: MonadTCM tcm => ModuleName -> tcm Nat | Source

Get the number of variables bound by anonymous modules.

withAnonymousModule :: MonadTCM tcm => ModuleName -> Nat -> tcm a -> tcm a | Source

Add variables bound by an anonymous module.

withEnv :: MonadTCM tcm => TCEnv -> tcm a -> tcm a | Source

Set the current environment to the given

getEnv :: MonadTCM tcm => tcm TCEnv | Source

Get the current environmnet
Produced by Haddock version 2.4.2