Agda.TypeChecking.Monad.Builtin
class HasBuiltins m
litType
setBuiltinThings
bindBuiltinName
bindPrimitive
getBuiltin
getBuiltin'
getPrimitive'
getPrimitive
constructorForm
constructorForm'
primInteger
primIntegerPos
primIntegerNegSuc
primFloat
primChar
primString
primUnit
primUnitUnit
primBool
primTrue
primFalse
primList
primNil
primCons
primIO
primNat
primSuc
primZero
primNatPlus
primNatMinus
primNatTimes
primNatDivSucAux
primNatModSucAux
primNatEquality
primNatLess
primSizeUniv
primSize
primSizeLt
primSizeSuc
primSizeInf
primSizeMax
primInf
primSharp
primFlat
primEquality
primRefl
primRewrite
primLevel
primLevelZero
primLevelSuc
primLevelMax
primFromNat
primFromNeg
primFromString
primQName
primArgInfo
primArgArgInfo
primArg
primArgArg
primAbs
primAbsAbs
primAgdaTerm
primAgdaTermVar
primAgdaTermLam
primAgdaTermExtLam
primAgdaTermDef
primAgdaTermCon
primAgdaTermPi
primAgdaTermSort
primAgdaTermLit
primAgdaTermUnsupported
primAgdaTermMeta
primAgdaErrorPart
primAgdaErrorPartString
primAgdaErrorPartTerm
primAgdaErrorPartName
primHiding
primHidden
primInstance
primVisible
primRelevance
primRelevant
primIrrelevant
primAgdaLiteral
primAgdaLitNat
primAgdaLitFloat
primAgdaLitString
primAgdaLitChar
primAgdaLitQName
primAgdaLitMeta
primAgdaSort
primAgdaSortSet
primAgdaSortLit
primAgdaSortUnsupported
primAgdaDefinition
primAgdaDefinitionFunDef
primAgdaDefinitionDataDef
primAgdaDefinitionRecordDef
primAgdaDefinitionPostulate
primAgdaDefinitionPrimitive
primAgdaDefinitionDataConstructor
primAgdaClause
primAgdaClauseClause
primAgdaClauseAbsurd
primAgdaPattern
primAgdaPatCon
primAgdaPatVar
primAgdaPatDot
primAgdaPatLit
primAgdaPatProj
primAgdaPatAbsurd
primAgdaMeta
primAgdaTCM
primAgdaTCMReturn
primAgdaTCMBind
primAgdaTCMUnify
primAgdaTCMTypeError
primAgdaTCMInferType
primAgdaTCMCheckType
primAgdaTCMNormalise
primAgdaTCMCatchError
primAgdaTCMGetContext
primAgdaTCMExtendContext
primAgdaTCMInContext
primAgdaTCMFreshName
primAgdaTCMDeclareDef
primAgdaTCMDefineFun
primAgdaTCMGetType
primAgdaTCMGetDefinition
primAgdaTCMQuoteTerm
primAgdaTCMUnquoteTerm
primAgdaTCMBlockOnMeta
primAgdaTCMCommit
builtinNat
builtinSuc
builtinZero
builtinNatPlus
builtinNatMinus
builtinNatTimes
builtinNatDivSucAux
builtinNatModSucAux
builtinNatEquals
builtinNatLess
builtinInteger
builtinIntegerPos
builtinIntegerNegSuc
builtinFloat
builtinChar
builtinString
builtinUnit
builtinUnitUnit
builtinBool
builtinTrue
builtinFalse
builtinList
builtinNil
builtinCons
builtinIO
builtinSizeUniv
builtinSize
builtinSizeLt
builtinSizeSuc
builtinSizeInf
builtinSizeMax
builtinInf
builtinSharp
builtinFlat
builtinEquality
builtinRefl
builtinRewrite
builtinLevelMax
builtinLevel
builtinLevelZero
builtinLevelSuc
builtinFromNat
builtinFromNeg
builtinFromString
builtinQName
builtinAgdaSort
builtinAgdaSortSet
builtinAgdaSortLit
builtinAgdaSortUnsupported
builtinHiding
builtinHidden
builtinInstance
builtinVisible
builtinRelevance
builtinRelevant
builtinIrrelevant
builtinArg
builtinArgInfo
builtinArgArgInfo
builtinArgArg
builtinAbs
builtinAbsAbs
builtinAgdaTerm
builtinAgdaTermVar
builtinAgdaTermLam
builtinAgdaTermExtLam
builtinAgdaTermDef
builtinAgdaTermCon
builtinAgdaTermPi
builtinAgdaTermSort
builtinAgdaTermLit
builtinAgdaTermUnsupported
builtinAgdaTermMeta
builtinAgdaErrorPart
builtinAgdaErrorPartString
builtinAgdaErrorPartTerm
builtinAgdaErrorPartName
builtinAgdaLiteral
builtinAgdaLitNat
builtinAgdaLitFloat
builtinAgdaLitChar
builtinAgdaLitString
builtinAgdaLitQName
builtinAgdaLitMeta
builtinAgdaClause
builtinAgdaClauseClause
builtinAgdaClauseAbsurd
builtinAgdaPattern
builtinAgdaPatVar
builtinAgdaPatCon
builtinAgdaPatDot
builtinAgdaPatLit
builtinAgdaPatProj
builtinAgdaPatAbsurd
builtinAgdaDefinitionFunDef
builtinAgdaDefinitionDataDef
builtinAgdaDefinitionRecordDef
builtinAgdaDefinitionDataConstructor
builtinAgdaDefinitionPostulate
builtinAgdaDefinitionPrimitive
builtinAgdaDefinition
builtinAgdaMeta
builtinAgdaTCM
builtinAgdaTCMReturn
builtinAgdaTCMBind
builtinAgdaTCMUnify
builtinAgdaTCMTypeError
builtinAgdaTCMInferType
builtinAgdaTCMCheckType
builtinAgdaTCMNormalise
builtinAgdaTCMCatchError
builtinAgdaTCMGetContext
builtinAgdaTCMExtendContext
builtinAgdaTCMInContext
builtinAgdaTCMFreshName
builtinAgdaTCMDeclareDef
builtinAgdaTCMDefineFun
builtinAgdaTCMGetType
builtinAgdaTCMGetDefinition
builtinAgdaTCMQuoteTerm
builtinAgdaTCMUnquoteTerm
builtinAgdaTCMBlockOnMeta
builtinAgdaTCMCommit
builtinsNoDef
data CoinductionKit
coinductionKit'
coinductionKit
primEqualityName
equalityView
equalityUnview