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