Agda.TypeChecking.Monad.Env

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.

withHighlightingLevel :: HighlightingLevel -> TCM a -> TCM a

Set highlighting level

doExpandLast :: TCM a -> TCM a

Restore setting for ExpandLast to default.

dontExpandLast :: TCM a -> TCM a

performedSimplification :: MonadReader TCEnv m => m a -> m a

If the reduced did a proper match (constructor or literal pattern), then record this as simplification step.

performedSimplification' :: MonadReader TCEnv m => Simplification -> m a -> m a

getSimplification :: MonadReader TCEnv m => m Simplification

Controlling reduction.

updateAllowedReductions :: (AllowedReductions -> AllowedReductions) -> TCEnv -> TCEnv

Lens for AllowedReductions.

modifyAllowedReductions :: (AllowedReductions -> AllowedReductions) -> TCM a -> TCM a

putAllowedReductions :: AllowedReductions -> TCM a -> TCM a

onlyReduceProjections :: TCM a -> TCM a

Reduce Def f vs only if f is a projection.

allowAllReductions :: TCM a -> TCM a

Allow all reductions except for non-terminating functions (default).

allowNonTerminatingReductions :: TCM a -> TCM a

Allow all reductions including non-terminating functions.

insideDotPattern :: TCM a -> TCM a

isInsideDotPattern :: TCM Bool

isReifyingUnquoted :: TCM Bool

nowReifyingUnquoted :: TCM a -> TCM a