Agda.TypeChecking.Monad.State

resetState

resetAllState

localTCState

localTCStateSaving

Lens for persistent states and its fields

lensPersistentState

updatePersistentState

modifyPersistentState

lensAccumStatisticsP

lensAccumStatistics

Scope

getScope

setScope

modifyScope_

modifyScope

withScope

withScope_

localScope

notInScope

printScope

Signature

Lens for stSignature and stImports

modifySignature

modifyImportedSignature

getSignature

getImportedSignature

modifyGlobalDefinition

setSignature

setImportedSignature

withSignature

Modifiers for rewrite rules

addRewriteRulesFor

Modifiers for parts of the signature

lookupDefinition

updateDefinitions

updateDefinition

updateTheDef

updateDefType

updateDefArgOccurrences

updateDefPolarity

updateDefCompiledRep

updateFunClauses

Top level module

setTopLevelModule

withTopLevelModule

Haskell imports

addHaskellImport

getHaskellImports

addHaskellImportUHC

getHaskellImportsUHC

addInlineHaskell

Interaction output callback

getInteractionOutputCallback

appInteractionOutputCallback

setInteractionOutputCallback

Pattern synonyms

getPatternSyns

setPatternSyns

modifyPatternSyns

getPatternSynImports

lookupPatternSyn

Benchmark

theBenchmark

updateBenchmark

getBenchmark

modifyBenchmark

freshTCM

Instance definitions

addSignatureInstances

updateInstanceDefs

modifyInstanceDefs

getAllInstanceDefs

getAnonInstanceDefs

clearAnonInstanceDefs

addUnknownInstance

addNamedInstance