Agda.TypeChecking.Monad.Builtin
litType
getBuiltinThing
setBuiltinThings
bindBuiltinName
bindPrimitive
getBuiltin
getBuiltin'
getPrimitive
primInteger
primAgdaRecordDef
primAgdaDataDef
primAgdaFunDef
primAgdaDefinitionDataConstructor
primAgdaDefinitionPrimitive
primAgdaDefinitionPostulate
primAgdaDefinitionRecordDef
primAgdaDefinitionDataDef
primAgdaDefinitionFunDef
primAgdaDefinition
primAgdaSortUnsupported
primAgdaSortLit
primAgdaSortSet
primAgdaSort
primIrrelevant
primRelevant
primRelevance
primVisible
primInstance
primHidden
primHiding
primAgdaTypeEl
primAgdaType
primAgdaTermUnsupported
primAgdaTermSort
primAgdaTermPi
primAgdaTermCon
primAgdaTermDef
primAgdaTermLam
primAgdaTermVar
primAgdaTerm
primArgArg
primArg
primQName
primIrrAxiom
primLevelMax
primLevelSuc
primLevelZero
primLevel
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
primSizeMax
builtinNat
builtinSuc
builtinZero
builtinNatPlus
builtinNatMinus
builtinNatTimes
builtinNatDivSucAux
builtinNatModSucAux
builtinNatEquals
builtinNatLess
builtinInteger
builtinFloat
builtinChar
builtinString
builtinBool
builtinTrue
builtinFalse
builtinList
builtinNil
builtinCons
builtinIO
builtinSize
builtinSizeLt
builtinSizeSuc
builtinSizeInf
builtinSizeMax
builtinInf
builtinSharp
builtinFlat
builtinEquality
builtinRefl
builtinLevelMax
builtinLevel
builtinLevelZero
builtinLevelSuc
builtinIrrAxiom
builtinQName
builtinAgdaSort
builtinAgdaSortSet
builtinAgdaSortLit
builtinAgdaSortUnsupported
builtinAgdaType
builtinAgdaTypeEl
builtinHiding
builtinHidden
builtinInstance
builtinVisible
builtinRelevance
builtinRelevant
builtinIrrelevant
builtinArg
builtinArgArg
builtinAgdaTerm
builtinAgdaTermVar
builtinAgdaTermLam
builtinAgdaTermDef
builtinAgdaTermCon
builtinAgdaTermPi
builtinAgdaTermSort
builtinAgdaTermUnsupported
builtinAgdaFunDef
builtinAgdaDataDef
builtinAgdaRecordDef
builtinAgdaDefinitionFunDef
builtinAgdaDefinitionDataDef
builtinAgdaDefinitionRecordDef
builtinAgdaDefinitionDataConstructor
builtinAgdaDefinitionPostulate
builtinAgdaDefinitionPrimitive
builtinAgdaDefinition
data CoinductionKit
coinductionKit