Agda.TypeChecking.Monad.Builtin

Documentation

getBuiltinThing :: String -> TCM (Maybe (Builtin PrimFun))

setBuiltinThings :: BuiltinThings PrimFun -> TCM ()

bindBuiltinName :: String -> Term -> TCM ()

bindPrimitive :: String -> PrimFun -> TCM ()

getBuiltin :: String -> TCM Term

getBuiltin' :: String -> TCM (Maybe Term)

getPrimitive :: String -> TCM PrimFun

The names of built-in things

primInteger, primAgdaRecordDef, primAgdaDataDef, primAgdaFunDef, primAgdaDefinitionDataConstructor, primAgdaDefinitionPrimitive, primAgdaDefinitionPostulate, primAgdaDefinitionRecordDef, primAgdaDefinitionDataDef, primAgdaDefinitionFunDef, primAgdaDefinition, primAgdaSortUnsupported, primAgdaSortLit, primAgdaSortSet, primAgdaSort, primIrrelevant, primRelevant, primRelvance, primVisible, primInstance, primHidden, primHiding, primAgdaTypeEl, primAgdaType, primAgdaTermUnsupported, primAgdaTermSort, primAgdaTermPi, primAgdaTermCon, primAgdaTermDef, primAgdaTermLam, primAgdaTermVar, primAgdaTerm, primArgArg, primArg, primQName, primLevelMax, primLevelSuc, primLevelZero, primLevel, primRefl, primEquality, primFlat, primSharp, primInf, primSizeInf, primSizeSuc, primSize, primNatLess, primNatEquality, primNatModSucAux, primNatDivSucAux, primNatTimes, primNatMinus, primNatPlus, primZero, primSuc, primNat, primIO, primCons, primNil, primList, primFalse, primTrue, primBool, primString, primChar, primFloat :: TCM Term