Safe Haskell | Safe-Infered |
---|
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
- 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
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]
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]
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]
builtinAgdaFunDef :: [Char]
builtinAgdaDataDef :: [Char]
builtinAgdaRecordDef :: [Char]