Agda.TypeChecking.Monad.Builtin
Contents
- 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
- primFloat :: TCM Term
- primChar :: TCM Term
- primString :: TCM Term
- primBool :: TCM Term
- primTrue :: TCM Term
- primFalse :: TCM Term
- primList :: TCM Term
- primNil :: TCM Term
- primCons :: TCM Term
- primIO :: TCM Term
- primNat :: TCM Term
- primSuc :: TCM Term
- primZero :: TCM Term
- primNatPlus :: TCM Term
- primNatMinus :: TCM Term
- primNatTimes :: TCM Term
- primNatDivSucAux :: TCM Term
- primNatModSucAux :: TCM Term
- primNatEquality :: TCM Term
- primNatLess :: TCM Term
- primSize :: TCM Term
- primSizeSuc :: TCM Term
- primSizeInf :: TCM Term
- primInf :: TCM Term
- primSharp :: TCM Term
- primFlat :: TCM Term
- primEquality :: TCM Term
- primRefl :: TCM Term
- primLevel :: TCM Term
- primLevelZero :: TCM Term
- primLevelSuc :: TCM Term
- primLevelMax :: TCM Term
- primQName :: TCM Term
- primArg :: TCM Term
- primArgArg :: TCM Term
- primAgdaTerm :: TCM Term
- primAgdaTermVar :: TCM Term
- primAgdaTermLam :: TCM Term
- primAgdaTermDef :: TCM Term
- primAgdaTermCon :: TCM Term
- primAgdaTermPi :: TCM Term
- primAgdaTermSort :: TCM Term
- primAgdaTermUnsupported :: TCM Term
- primAgdaType :: TCM Term
- primAgdaTypeEl :: TCM Term
- primHiding :: TCM Term
- primHidden :: TCM Term
- primInstance :: TCM Term
- primVisible :: TCM Term
- primRelvance :: TCM Term
- primRelevant :: TCM Term
- primIrrelevant :: TCM Term
- primAgdaSort :: TCM Term
- primAgdaSortSet :: TCM Term
- primAgdaSortLit :: TCM Term
- primAgdaSortUnsupported :: TCM Term
- primAgdaDefinition :: TCM Term
- primAgdaDefinitionFunDef :: TCM Term
- primAgdaDefinitionDataDef :: TCM Term
- primAgdaDefinitionRecordDef :: TCM Term
- primAgdaDefinitionPostulate :: TCM Term
- primAgdaDefinitionPrimitive :: TCM Term
- primAgdaDefinitionDataConstructor :: TCM Term
- primAgdaFunDef :: TCM Term
- primAgdaDataDef :: TCM Term
- primAgdaRecordDef :: TCM Term
- primInteger :: TCM Term
Documentation
getBuiltin :: String -> TCM TermSource
getPrimitive :: String -> TCM PrimFunSource