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.6.0