Agda.TypeChecking.Monad.Builtin
class HasBuiltins m
litType
setBuiltinThings
bindBuiltinName
bindPrimitive
getBuiltin
getBuiltin'
getPrimitive'
getPrimitive
constructorForm
constructorForm'
primInteger
primAgdaPatAbsurd
primAgdaPatProj
primAgdaPatLit
primAgdaRecordDef
primAgdaDataDef
primAgdaPatDot
primAgdaPatVar
primAgdaPatCon
primAgdaPattern
primAgdaClauseAbsurd
primAgdaClauseClause
primAgdaClause
primAgdaFunDefCon
primAgdaFunDef
primAgdaDefinitionDataConstructor
primAgdaDefinitionPrimitive
primAgdaDefinitionPostulate
primAgdaDefinitionRecordDef
primAgdaDefinitionDataDef
primAgdaDefinitionFunDef
primAgdaDefinition
primAgdaSortUnsupported
primAgdaSortLit
primAgdaSortSet
primAgdaSort
primAgdaLitQName
primAgdaLitChar
primAgdaLitString
primAgdaLitFloat
primAgdaLitNat
primAgdaLiteral
primIrrelevant
primRelevant
primRelevance
primVisible
primInstance
primHidden
primHiding
primAgdaTypeEl
primAgdaType
primAgdaTermUnsupported
primAgdaTermLit
primAgdaTermSort
primAgdaTermPi
primAgdaTermCon
primAgdaTermDef
primAgdaTermExtLam
primAgdaTermLam
primAgdaTermVar
primAgdaTerm
primArgArg
primArg
primArgArgInfo
primArgInfo
primQName
primSizeMax
primIrrAxiom
primLevelMax
primLevelSuc
primLevelZero
primLevel
primRewrite
primRefl
primEquality
primFlat
primSharp
primInf
primSizeInf
primSizeSuc
primSizeLt
primSize
primNatLess
primNatEquality
primNatModSucAux
primNatDivSucAux
primNatTimes
primNatMinus
primNatPlus
primZero
primSuc
primNat
primIO
primCons
primNil
primList
primFalse
primTrue
primBool
primString
primChar
primFloat
builtinNat
builtinAgdaDefinition
builtinAgdaDefinitionPrimitive
builtinAgdaDefinitionPostulate
builtinAgdaDefinitionDataConstructor
builtinAgdaDefinitionRecordDef
builtinAgdaDefinitionDataDef
builtinAgdaDefinitionFunDef
builtinAgdaRecordDef
builtinAgdaDataDef
builtinAgdaPatAbsurd
builtinAgdaPatProj
builtinAgdaPatLit
builtinAgdaPatDot
builtinAgdaPatCon
builtinAgdaPatVar
builtinAgdaPattern
builtinAgdaClauseAbsurd
builtinAgdaClauseClause
builtinAgdaClause
builtinAgdaFunDefCon
builtinAgdaFunDef
builtinAgdaLitQName
builtinAgdaLitString
builtinAgdaLitChar
builtinAgdaLitFloat
builtinAgdaLitNat
builtinAgdaLiteral
builtinAgdaTermUnsupported
builtinAgdaTermLit
builtinAgdaTermSort
builtinAgdaTermPi
builtinAgdaTermCon
builtinAgdaTermDef
builtinAgdaTermExtLam
builtinAgdaTermLam
builtinAgdaTermVar
builtinAgdaTerm
builtinArgArg
builtinArgArgInfo
builtinArgInfo
builtinArg
builtinIrrelevant
builtinRelevant
builtinRelevance
builtinVisible
builtinInstance
builtinHidden
builtinHiding
builtinAgdaTypeEl
builtinAgdaType
builtinAgdaSortUnsupported
builtinAgdaSortLit
builtinAgdaSortSet
builtinAgdaSort
builtinQName
builtinIrrAxiom
builtinLevelSuc
builtinLevelZero
builtinLevel
builtinLevelMax
builtinRewrite
builtinRefl
builtinEquality
builtinFlat
builtinSharp
builtinInf
builtinSizeMax
builtinSizeInf
builtinSizeSuc
builtinSizeLt
builtinSize
builtinIO
builtinCons
builtinNil
builtinList
builtinFalse
builtinTrue
builtinBool
builtinString
builtinChar
builtinFloat
builtinInteger
builtinNatLess
builtinNatEquals
builtinNatModSucAux
builtinNatDivSucAux
builtinNatTimes
builtinNatMinus
builtinNatPlus
builtinZero
builtinSuc
data CoinductionKit
coinductionKit
primEqualityName