Agda.TypeChecking.Monad.Signature
addConstant
setTerminates
modifyFunClauses
addClauses
addHaskellCode
addHaskellExport
addHaskellType
addEpicCode
addJSCode
markStatic
unionSignatures
addSection
lookupSection
addDisplayForms
applySection
applySection'
addDisplayForm
canonicalName
sameDef
whatInduction
singleConstructorType
class HasConstInfo m
defaultGetRewriteRulesFor
getConInfo
getPolarity
getPolarity'
setPolarity
getArgOccurrence
setArgOccurrences
modifyArgOccurrences
getMutual
setMutual
mutuallyRecursive
getSection
getCurrentModuleFreeVars
getDefFreeVars
freeVarsToApply
instantiateDef
makeAbstract
inAbstractMode
inConcreteMode
ignoreAbstractMode
inConcreteOrAbstractMode
treatAbstractly
treatAbstractly'
typeOfConst
relOfConst
colOfConst
sortOfConst
defPars
droppedPars
isProjection
isProjection_
isProperProjection
projectionArgs
usesCopatterns
applyDef
getDefType