Agda-2.3.0.1: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Infered

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

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

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]