Agda.TypeChecking.Monad.Builtin

getBuiltinThing

setBuiltinThings

bindBuiltinName

bindPrimitive

getBuiltin

getBuiltin'

getPrimitive

The names of built-in things

primFloat

primChar

primString

primBool

primTrue

primFalse

primList

primNil

primCons

primIO

primNat

primSuc

primZero

primNatPlus

primNatMinus

primNatTimes

primNatDivSucAux

primNatModSucAux

primNatEquality

primNatLess

primSize

primSizeSuc

primSizeInf

primInf

primSharp

primFlat

primEquality

primRefl

primLevel

primLevelZero

primLevelSuc

primLevelMax

primQName

primArg

primArgArg

primAgdaTerm

primAgdaTermVar

primAgdaTermLam

primAgdaTermDef

primAgdaTermCon

primAgdaTermPi

primAgdaTermSort

primAgdaTermUnsupported

primAgdaType

primAgdaTypeEl

primHiding

primHidden

primInstance

primVisible

primRelvance

primRelevant

primIrrelevant

primAgdaSort

primAgdaSortSet

primAgdaSortLit

primAgdaSortUnsupported

primAgdaDefinition

primAgdaDefinitionFunDef

primAgdaDefinitionDataDef

primAgdaDefinitionRecordDef

primAgdaDefinitionPostulate

primAgdaDefinitionPrimitive

primAgdaDefinitionDataConstructor

primAgdaFunDef

primAgdaDataDef

primAgdaRecordDef

primInteger