Agda.TypeChecking.Monad.Builtin

class HasBuiltins m

litType

setBuiltinThings

bindBuiltinName

bindPrimitive

getBuiltin

getBuiltin'

getPrimitive'

getPrimitive

constructorForm

constructorForm'

The names of built-in things

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

Builtin equality

primEqualityName