Safe Haskell | None |
---|---|
Language | Haskell98 |
- class (Functor m, Applicative m, Monad m) => HasBuiltins m where
- getBuiltinThing :: String -> m (Maybe (Builtin PrimFun))
- litType :: Literal -> TCM Type
- setBuiltinThings :: BuiltinThings PrimFun -> TCM ()
- bindBuiltinName :: String -> Term -> TCM ()
- bindPrimitive :: String -> PrimFun -> TCM ()
- getBuiltin :: String -> TCM Term
- getBuiltin' :: HasBuiltins m => String -> m (Maybe Term)
- getPrimitive' :: HasBuiltins m => String -> m (Maybe PrimFun)
- getPrimitive :: String -> TCM PrimFun
- constructorForm :: Term -> TCM Term
- constructorForm' :: Applicative m => m Term -> m Term -> Term -> m Term
- 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
- primArgArgInfo :: TCM Term
- primArgInfo :: TCM Term
- primQName :: TCM Term
- primSizeMax :: 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
- 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]
- builtinArgInfo :: [Char]
- builtinArgArgInfo :: [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)
- primEqualityName :: TCM QName
Documentation
class (Functor m, Applicative m, Monad m) => HasBuiltins m where Source
HasBuiltins ReduceM | |
MonadIO m => HasBuiltins (TCMT m) |
setBuiltinThings :: BuiltinThings PrimFun -> TCM () Source
bindBuiltinName :: String -> Term -> TCM () Source
bindPrimitive :: String -> PrimFun -> TCM () Source
getBuiltin :: String -> TCM Term Source
getBuiltin' :: HasBuiltins m => String -> m (Maybe Term) Source
getPrimitive' :: HasBuiltins m => String -> m (Maybe PrimFun) Source
getPrimitive :: String -> TCM PrimFun Source
constructorForm :: Term -> TCM Term Source
Rewrite a literal to constructor form if possible.
constructorForm' :: Applicative m => m Term -> m Term -> Term -> m Term Source
The names of built-in things
primInteger :: TCM Term Source
primVisible :: TCM Term Source
primHidden :: TCM Term Source
primHiding :: TCM Term Source
primArgArg :: TCM Term Source
primArgInfo :: TCM Term Source
primSizeMax :: TCM Term Source
primSizeInf :: TCM Term Source
primSizeSuc :: TCM Term Source
primSizeLt :: TCM Term Source
primNatLess :: TCM Term Source
primNatPlus :: TCM Term Source
primString :: TCM Term Source
builtinNat :: [Char] Source
builtinSuc :: [Char] Source
builtinZero :: [Char] Source
builtinNatPlus :: [Char] Source
builtinNatMinus :: [Char] Source
builtinNatTimes :: [Char] Source
builtinNatEquals :: [Char] Source
builtinNatLess :: [Char] Source
builtinInteger :: [Char] Source
builtinFloat :: [Char] Source
builtinChar :: [Char] Source
builtinString :: [Char] Source
builtinBool :: [Char] Source
builtinTrue :: [Char] Source
builtinFalse :: [Char] Source
builtinList :: [Char] Source
builtinNil :: [Char] Source
builtinCons :: [Char] Source
builtinSize :: [Char] Source
builtinSizeLt :: [Char] Source
builtinSizeSuc :: [Char] Source
builtinSizeInf :: [Char] Source
builtinSizeMax :: [Char] Source
builtinInf :: [Char] Source
builtinSharp :: [Char] Source
builtinFlat :: [Char] Source
builtinEquality :: [Char] Source
builtinRefl :: [Char] Source
builtinLevelMax :: [Char] Source
builtinLevel :: [Char] Source
builtinLevelZero :: [Char] Source
builtinLevelSuc :: [Char] Source
builtinIrrAxiom :: [Char] Source
builtinQName :: [Char] Source
builtinAgdaSort :: [Char] Source
builtinAgdaSortSet :: [Char] Source
builtinAgdaSortLit :: [Char] Source
builtinAgdaType :: [Char] Source
builtinAgdaTypeEl :: [Char] Source
builtinHiding :: [Char] Source
builtinHidden :: [Char] Source
builtinInstance :: [Char] Source
builtinVisible :: [Char] Source
builtinRelevance :: [Char] Source
builtinRelevant :: [Char] Source
builtinIrrelevant :: [Char] Source
builtinArg :: [Char] Source
builtinArgInfo :: [Char] Source
builtinArgArgInfo :: [Char] Source
builtinArgArg :: [Char] Source
builtinAgdaTerm :: [Char] Source
builtinAgdaTermVar :: [Char] Source
builtinAgdaTermLam :: [Char] Source
builtinAgdaTermDef :: [Char] Source
builtinAgdaTermCon :: [Char] Source
builtinAgdaTermPi :: [Char] Source
builtinAgdaFunDef :: [Char] Source
builtinAgdaDataDef :: [Char] Source
data CoinductionKit Source
The coinductive primitives.
CoinductionKit | |
|
coinductionKit :: TCM (Maybe CoinductionKit) Source
Tries to build a CoinductionKit
.
Builtin equality
primEqualityName :: TCM QName Source
Get the name of the equality type.