Agda.TypeChecking.Monad.Builtin

Contents

• The names of built-in things

Synopsis

• 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
• builtinNat :: [Char]
• builtinSuc :: [Char]
• builtinZero :: [Char]
• builtinNatPlus :: [Char]
• builtinNatMinus :: [Char]
• builtinNatTimes :: [Char]
• builtinNatDivSucAux :: [Char]
• builtinNatModSucAux :: [Char]
• builtinNatEquals :: [Char]
• builtinNatLess :: [Char]
• builtinInteger :: [Char]
• builtinFloat :: [Char]
• builtinChar :: [Char]
• builtinString :: [Char]
• builtinBool :: [Char]
• builtinTrue :: [Char]
• builtinFalse :: [Char]
• builtinList :: [Char]
• builtinNil :: [Char]
• builtinCons :: [Char]
• builtinIO :: [Char]
• builtinSize :: [Char]
• builtinSizeSuc :: [Char]
• builtinSizeInf :: [Char]
• builtinInf :: [Char]
• builtinSharp :: [Char]
• builtinFlat :: [Char]
• builtinEquality :: [Char]
• builtinRefl :: [Char]
• builtinLevelMax :: [Char]
• builtinLevel :: [Char]
• builtinLevelZero :: [Char]
• builtinLevelSuc :: [Char]
• builtinQName :: [Char]
• builtinAgdaSort :: [Char]
• builtinAgdaSortSet :: [Char]
• builtinAgdaSortLit :: [Char]
• builtinAgdaSortUnsupported :: [Char]
• builtinAgdaType :: [Char]
• builtinAgdaTypeEl :: [Char]
• builtinHiding :: [Char]
• builtinHidden :: [Char]
• builtinInstance :: [Char]
• builtinVisible :: [Char]
• builtinRelevance :: [Char]
• builtinRelevant :: [Char]
• builtinIrrelevant :: [Char]
• builtinArg :: [Char]
• builtinArgArg :: [Char]
• builtinAgdaTerm :: [Char]
• builtinAgdaTermVar :: [Char]
• builtinAgdaTermLam :: [Char]
• builtinAgdaTermDef :: [Char]
• builtinAgdaTermCon :: [Char]
• builtinAgdaTermPi :: [Char]
• builtinAgdaTermSort :: [Char]
• builtinAgdaTermUnsupported :: [Char]
• builtinAgdaFunDef :: [Char]
• builtinAgdaDataDef :: [Char]
• builtinAgdaRecordDef :: [Char]
• builtinAgdaDefinitionFunDef :: [Char]
• builtinAgdaDefinitionDataDef :: [Char]
• builtinAgdaDefinitionRecordDef :: [Char]
• builtinAgdaDefinitionDataConstructor :: [Char]
• builtinAgdaDefinitionPostulate :: [Char]
• builtinAgdaDefinitionPrimitive :: [Char]
• builtinAgdaDefinition :: [Char]

Documentation

The names of built-in things