- 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
- 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
Documentation
getBuiltin :: String -> TCM TermSource
getPrimitive :: String -> TCM PrimFunSource
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 TermSource