Safe Haskell | None |
---|
Agda.TypeChecking.Monad.Builtin
Contents
- litType :: Literal -> TCM Type
- 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 :: TCM Term
- primAgdaRecordDef :: TCM Term
- primAgdaDataDef :: TCM Term
- primAgdaFunDef :: TCM Term
- primAgdaDefinitionDataConstructor :: TCM Term
- primAgdaDefinitionPrimitive :: TCM Term
- primAgdaDefinitionPostulate :: TCM Term
- primAgdaDefinitionRecordDef :: TCM Term
- primAgdaDefinitionDataDef :: TCM Term
- primAgdaDefinitionFunDef :: TCM Term
- primAgdaDefinition :: TCM Term
- primAgdaSortUnsupported :: TCM Term
- primAgdaSortLit :: TCM Term
- primAgdaSortSet :: TCM Term
- primAgdaSort :: TCM Term
- primIrrelevant :: TCM Term
- primRelevant :: TCM Term
- primRelevance :: TCM Term
- primVisible :: TCM Term
- primInstance :: TCM Term
- primHidden :: TCM Term
- primHiding :: TCM Term
- primAgdaTypeEl :: TCM Term
- primAgdaType :: TCM Term
- primAgdaTermUnsupported :: TCM Term
- primAgdaTermSort :: TCM Term
- primAgdaTermPi :: TCM Term
- primAgdaTermCon :: TCM Term
- primAgdaTermDef :: TCM Term
- primAgdaTermLam :: TCM Term
- primAgdaTermVar :: TCM Term
- primAgdaTerm :: TCM Term
- primArgArg :: TCM Term
- primArg :: TCM Term
- primQName :: TCM Term
- primIrrAxiom :: TCM Term
- primLevelMax :: TCM Term
- primLevelSuc :: TCM Term
- primLevelZero :: TCM Term
- primLevel :: TCM Term
- primRefl :: TCM Term
- primEquality :: TCM Term
- primFlat :: TCM Term
- primSharp :: TCM Term
- primInf :: TCM Term
- primSizeInf :: TCM Term
- primSizeSuc :: TCM Term
- primSizeLt :: TCM Term
- primSize :: TCM Term
- primNatLess :: TCM Term
- primNatEquality :: TCM Term
- primNatModSucAux :: TCM Term
- primNatDivSucAux :: TCM Term
- primNatTimes :: TCM Term
- primNatMinus :: TCM Term
- primNatPlus :: TCM Term
- primZero :: TCM Term
- primSuc :: TCM Term
- primNat :: TCM Term
- primIO :: TCM Term
- primCons :: TCM Term
- primNil :: TCM Term
- primList :: TCM Term
- primFalse :: TCM Term
- primTrue :: TCM Term
- primBool :: TCM Term
- primString :: TCM Term
- primChar :: TCM Term
- primFloat :: TCM Term
- primSizeMax :: 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]
- builtinSizeLt :: [Char]
- builtinSizeSuc :: [Char]
- builtinSizeInf :: [Char]
- builtinSizeMax :: [Char]
- builtinInf :: [Char]
- builtinSharp :: [Char]
- builtinFlat :: [Char]
- builtinEquality :: [Char]
- builtinRefl :: [Char]
- builtinLevelMax :: [Char]
- builtinLevel :: [Char]
- builtinLevelZero :: [Char]
- builtinLevelSuc :: [Char]
- builtinIrrAxiom :: [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]
- data CoinductionKit = CoinductionKit {
- nameOfInf :: QName
- nameOfSharp :: QName
- nameOfFlat :: QName
- coinductionKit :: TCM (Maybe CoinductionKit)
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 :: TCM Term
primAgdaSort :: TCM Term
primRelevant :: TCM Term
primRelevance :: TCM Term
primVisible :: TCM Term
primInstance :: TCM Term
primHidden :: TCM Term
primHiding :: TCM Term
primAgdaType :: TCM Term
primAgdaTerm :: TCM Term
primArgArg :: TCM Term
primIrrAxiom :: TCM Term
primLevelMax :: TCM Term
primLevelSuc :: TCM Term
primLevelZero :: TCM Term
primEquality :: TCM Term
primSizeInf :: TCM Term
primSizeSuc :: TCM Term
primSizeLt :: TCM Term
primNatLess :: TCM Term
primNatTimes :: TCM Term
primNatMinus :: TCM Term
primNatPlus :: TCM Term
primString :: TCM Term
primSizeMax :: 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]
builtinSizeLt :: [Char]
builtinSizeSuc :: [Char]
builtinSizeInf :: [Char]
builtinSizeMax :: [Char]
builtinInf :: [Char]
builtinSharp :: [Char]
builtinFlat :: [Char]
builtinEquality :: [Char]
builtinRefl :: [Char]
builtinLevelMax :: [Char]
builtinLevel :: [Char]
builtinLevelZero :: [Char]
builtinLevelSuc :: [Char]
builtinIrrAxiom :: [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]
data CoinductionKit
The coinductive primitives.
Constructors
CoinductionKit | |
Fields
|
coinductionKit :: TCM (Maybe CoinductionKit)
Tries to build a CoinductionKit
.