Safe Haskell | None |
---|---|
Language | Haskell98 |
Agda.TypeChecking.Monad.Builtin
- 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
- primFloat :: TCM Term
- primChar :: TCM Term
- primString :: TCM Term
- primBool :: TCM Term
- primTrue :: TCM Term
- primFalse :: TCM Term
- primList :: TCM Term
- primNil :: TCM Term
- primCons :: TCM Term
- primIO :: TCM Term
- primNat :: TCM Term
- primSuc :: TCM Term
- primZero :: TCM Term
- primNatPlus :: TCM Term
- primNatMinus :: TCM Term
- primNatTimes :: TCM Term
- primNatDivSucAux :: TCM Term
- primNatModSucAux :: TCM Term
- primNatEquality :: TCM Term
- primNatLess :: TCM Term
- primSizeUniv :: TCM Term
- primSize :: TCM Term
- primSizeLt :: TCM Term
- primSizeSuc :: TCM Term
- primSizeInf :: TCM Term
- primSizeMax :: TCM Term
- primInf :: TCM Term
- primSharp :: TCM Term
- primFlat :: TCM Term
- primEquality :: TCM Term
- primRefl :: TCM Term
- primRewrite :: TCM Term
- primLevel :: TCM Term
- primLevelZero :: TCM Term
- primLevelSuc :: TCM Term
- primLevelMax :: TCM Term
- primIrrAxiom :: TCM Term
- primQName :: TCM Term
- primArgInfo :: TCM Term
- primArgArgInfo :: TCM Term
- primArg :: TCM Term
- primArgArg :: TCM Term
- primAgdaTerm :: TCM Term
- primAgdaTermVar :: TCM Term
- primAgdaTermLam :: TCM Term
- primAgdaTermExtLam :: TCM Term
- primAgdaTermDef :: TCM Term
- primAgdaTermCon :: TCM Term
- primAgdaTermPi :: TCM Term
- primAgdaTermSort :: TCM Term
- primAgdaTermLit :: TCM Term
- primAgdaTermUnsupported :: TCM Term
- primAgdaType :: TCM Term
- primAgdaTypeEl :: TCM Term
- primHiding :: TCM Term
- primHidden :: TCM Term
- primInstance :: TCM Term
- primVisible :: TCM Term
- primRelevance :: TCM Term
- primRelevant :: TCM Term
- primIrrelevant :: TCM Term
- primAgdaLiteral :: TCM Term
- primAgdaLitNat :: TCM Term
- primAgdaLitFloat :: TCM Term
- primAgdaLitString :: TCM Term
- primAgdaLitChar :: TCM Term
- primAgdaLitQName :: TCM Term
- primAgdaSort :: TCM Term
- primAgdaSortSet :: TCM Term
- primAgdaSortLit :: TCM Term
- primAgdaSortUnsupported :: TCM Term
- primAgdaDefinition :: TCM Term
- primAgdaDefinitionFunDef :: TCM Term
- primAgdaDefinitionDataDef :: TCM Term
- primAgdaDefinitionRecordDef :: TCM Term
- primAgdaDefinitionPostulate :: TCM Term
- primAgdaDefinitionPrimitive :: TCM Term
- primAgdaDefinitionDataConstructor :: TCM Term
- primAgdaFunDef :: TCM Term
- primAgdaFunDefCon :: TCM Term
- primAgdaClause :: TCM Term
- primAgdaClauseClause :: TCM Term
- primAgdaClauseAbsurd :: TCM Term
- primAgdaPattern :: TCM Term
- primAgdaPatCon :: TCM Term
- primAgdaPatVar :: TCM Term
- primAgdaPatDot :: TCM Term
- primAgdaDataDef :: TCM Term
- primAgdaRecordDef :: TCM Term
- primAgdaPatLit :: TCM Term
- primAgdaPatProj :: TCM Term
- primAgdaPatAbsurd :: TCM Term
- builtinNat :: String
- builtinSuc :: String
- builtinZero :: String
- builtinNatPlus :: String
- builtinNatMinus :: String
- builtinNatTimes :: String
- builtinNatDivSucAux :: String
- builtinNatModSucAux :: String
- builtinNatEquals :: String
- builtinNatLess :: String
- builtinInteger :: String
- builtinFloat :: String
- builtinChar :: String
- builtinString :: String
- builtinBool :: String
- builtinTrue :: String
- builtinFalse :: String
- builtinList :: String
- builtinNil :: String
- builtinCons :: String
- builtinIO :: String
- builtinSizeUniv :: String
- builtinSize :: String
- builtinSizeLt :: String
- builtinSizeSuc :: String
- builtinSizeInf :: String
- builtinSizeMax :: String
- builtinInf :: String
- builtinSharp :: String
- builtinFlat :: String
- builtinEquality :: String
- builtinRefl :: String
- builtinRewrite :: String
- builtinLevelMax :: String
- builtinLevel :: String
- builtinLevelZero :: String
- builtinLevelSuc :: String
- builtinIrrAxiom :: String
- builtinQName :: String
- builtinAgdaSort :: String
- builtinAgdaSortSet :: String
- builtinAgdaSortLit :: String
- builtinAgdaSortUnsupported :: String
- builtinAgdaType :: String
- builtinAgdaTypeEl :: String
- builtinHiding :: String
- builtinHidden :: String
- builtinInstance :: String
- builtinVisible :: String
- builtinRelevance :: String
- builtinRelevant :: String
- builtinIrrelevant :: String
- builtinArg :: String
- builtinArgInfo :: String
- builtinArgArgInfo :: String
- builtinArgArg :: String
- builtinAgdaTerm :: String
- builtinAgdaTermVar :: String
- builtinAgdaTermLam :: String
- builtinAgdaTermExtLam :: String
- builtinAgdaTermDef :: String
- builtinAgdaTermCon :: String
- builtinAgdaTermPi :: String
- builtinAgdaTermSort :: String
- builtinAgdaTermLit :: String
- builtinAgdaTermUnsupported :: String
- builtinAgdaLiteral :: String
- builtinAgdaLitNat :: String
- builtinAgdaLitFloat :: String
- builtinAgdaLitChar :: String
- builtinAgdaLitString :: String
- builtinAgdaLitQName :: String
- builtinAgdaFunDef :: String
- builtinAgdaFunDefCon :: String
- builtinAgdaClause :: String
- builtinAgdaClauseClause :: String
- builtinAgdaClauseAbsurd :: String
- builtinAgdaPattern :: String
- builtinAgdaPatVar :: String
- builtinAgdaPatCon :: String
- builtinAgdaPatDot :: String
- builtinAgdaPatLit :: String
- builtinAgdaPatProj :: String
- builtinAgdaPatAbsurd :: String
- builtinAgdaDataDef :: String
- builtinAgdaRecordDef :: String
- builtinAgdaDefinitionFunDef :: String
- builtinAgdaDefinitionDataDef :: String
- builtinAgdaDefinitionRecordDef :: String
- builtinAgdaDefinitionDataConstructor :: String
- builtinAgdaDefinitionPostulate :: String
- builtinAgdaDefinitionPrimitive :: String
- builtinAgdaDefinition :: String
- builtinsNoDef :: [String]
- 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
Methods
getBuiltinThing :: String -> m (Maybe (Builtin PrimFun))
Instances
MonadIO m => HasBuiltins (TCMT m) |
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
Rewrite a literal to constructor form if possible.
constructorForm' :: Applicative m => m Term -> m Term -> Term -> m Term
The names of built-in things
primInteger :: TCM Term
primString :: TCM Term
primNatPlus :: TCM Term
primNatMinus :: TCM Term
primNatTimes :: TCM Term
primNatLess :: TCM Term
primSizeUniv :: TCM Term
primSizeLt :: TCM Term
primSizeSuc :: TCM Term
primSizeInf :: TCM Term
primSizeMax :: TCM Term
primEquality :: TCM Term
primRewrite :: TCM Term
primLevelZero :: TCM Term
primLevelSuc :: TCM Term
primLevelMax :: TCM Term
primIrrAxiom :: TCM Term
primArgInfo :: TCM Term
primArgArg :: TCM Term
primAgdaTerm :: TCM Term
primAgdaType :: TCM Term
primHiding :: TCM Term
primHidden :: TCM Term
primInstance :: TCM Term
primVisible :: TCM Term
primRelevance :: TCM Term
primRelevant :: TCM Term
primAgdaSort :: TCM Term
builtinNat :: String
builtinSuc :: String
builtinNil :: String
builtinInf :: String
builtinArg :: String
builtinsNoDef :: [String]
data CoinductionKit
The coinductive primitives.
Constructors
CoinductionKit | |
Fields
|
coinductionKit :: TCM (Maybe CoinductionKit)
Tries to build a CoinductionKit
.
Builtin equality
Get the name of the equality type.