Agda.TypeChecking.Monad.Env

currentModule

withCurrentModule

getAnonymousVariables

withAnonymousModule

withEnv

getEnv

withIncreasedModuleNestingLevel

withHighlightingLevel

doExpandLast

dontExpandLast

performedSimplification

performedSimplification'

getSimplification

Controlling reduction.

updateAllowedReductions

modifyAllowedReductions

putAllowedReductions

onlyReduceProjections

allowAllReductions

allowNonTerminatingReductions

insideDotPattern

isInsideDotPattern

isReifyingUnquoted

nowReifyingUnquoted