| Safe Haskell | None |
|---|
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
- primAgdaRecordDef :: TCM Term
- primAgdaDataDef :: TCM Term
- primAgdaPatDot :: TCM Term
- primAgdaPatVar :: TCM Term
- primAgdaPatCon :: TCM Term
- primAgdaPattern :: TCM Term
- primAgdaClauseAbsurd :: TCM Term
- primAgdaClauseClause :: TCM Term
- primAgdaClause :: TCM Term
- primAgdaFunDefCon :: 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
- primAgdaLitQName :: TCM Term
- primAgdaLitChar :: TCM Term
- primAgdaLitString :: TCM Term
- primAgdaLitFloat :: TCM Term
- primAgdaLitNat :: TCM Term
- primAgdaLiteral :: 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
- primAgdaTermLit :: TCM Term
- primAgdaTermSort :: TCM Term
- primAgdaTermPi :: TCM Term
- primAgdaTermCon :: TCM Term
- primAgdaTermDef :: TCM Term
- primAgdaTermExtLam :: 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
- primRewrite :: 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
- primAgdaPatLit :: TCM Term
- primAgdaPatProj :: TCM Term
- primAgdaPatAbsurd :: 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]
- builtinRewrite :: [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]
- builtinAgdaTermExtLam :: [Char]
- builtinAgdaTermDef :: [Char]
- builtinAgdaTermCon :: [Char]
- builtinAgdaTermPi :: [Char]
- builtinAgdaTermSort :: [Char]
- builtinAgdaTermLit :: [Char]
- builtinAgdaTermUnsupported :: [Char]
- builtinAgdaLiteral :: [Char]
- builtinAgdaLitNat :: [Char]
- builtinAgdaLitFloat :: [Char]
- builtinAgdaLitChar :: [Char]
- builtinAgdaLitString :: [Char]
- builtinAgdaLitQName :: [Char]
- builtinAgdaFunDef :: [Char]
- builtinAgdaFunDefCon :: [Char]
- builtinAgdaClause :: [Char]
- builtinAgdaClauseClause :: [Char]
- builtinAgdaClauseAbsurd :: [Char]
- builtinAgdaPattern :: [Char]
- builtinAgdaPatVar :: [Char]
- builtinAgdaPatCon :: [Char]
- builtinAgdaPatDot :: [Char]
- builtinAgdaPatLit :: [Char]
- builtinAgdaPatProj :: [Char]
- builtinAgdaPatAbsurd :: [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 whereSource
Methods
getBuiltinThing :: String -> m (Maybe (Builtin PrimFun))Source
Instances
| 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 TermSource
getBuiltin' :: HasBuiltins m => String -> m (Maybe Term)Source
getPrimitive' :: HasBuiltins m => String -> m (Maybe PrimFun)Source
getPrimitive :: String -> TCM PrimFunSource
constructorForm :: Term -> TCM TermSource
Rewrite a literal to constructor form if possible.
The names of built-in things
builtinNat :: [Char]Source
builtinSuc :: [Char]Source
builtinZero :: [Char]Source
builtinNatPlus :: [Char]Source
builtinNatMinus :: [Char]Source
builtinNatTimes :: [Char]Source
builtinNatDivSucAux :: [Char]Source
builtinNatModSucAux :: [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
builtinRewrite :: [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
builtinAgdaSortUnsupported :: [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
builtinAgdaTermExtLam :: [Char]Source
builtinAgdaTermDef :: [Char]Source
builtinAgdaTermCon :: [Char]Source
builtinAgdaTermPi :: [Char]Source
builtinAgdaTermSort :: [Char]Source
builtinAgdaTermLit :: [Char]Source
builtinAgdaTermUnsupported :: [Char]Source
builtinAgdaLiteral :: [Char]Source
builtinAgdaLitNat :: [Char]Source
builtinAgdaLitFloat :: [Char]Source
builtinAgdaLitChar :: [Char]Source
builtinAgdaLitString :: [Char]Source
builtinAgdaLitQName :: [Char]Source
builtinAgdaFunDef :: [Char]Source
builtinAgdaFunDefCon :: [Char]Source
builtinAgdaClause :: [Char]Source
builtinAgdaClauseClause :: [Char]Source
builtinAgdaClauseAbsurd :: [Char]Source
builtinAgdaPattern :: [Char]Source
builtinAgdaPatVar :: [Char]Source
builtinAgdaPatCon :: [Char]Source
builtinAgdaPatDot :: [Char]Source
builtinAgdaPatLit :: [Char]Source
builtinAgdaPatProj :: [Char]Source
builtinAgdaPatAbsurd :: [Char]Source
builtinAgdaDataDef :: [Char]Source
builtinAgdaRecordDef :: [Char]Source
builtinAgdaDefinitionFunDef :: [Char]Source
builtinAgdaDefinitionDataDef :: [Char]Source
builtinAgdaDefinitionRecordDef :: [Char]Source
builtinAgdaDefinitionPostulate :: [Char]Source
builtinAgdaDefinitionPrimitive :: [Char]Source
builtinAgdaDefinition :: [Char]Source
data CoinductionKit Source
The coinductive primitives.
Constructors
| CoinductionKit | |
Fields
| |
coinductionKit :: TCM (Maybe CoinductionKit)Source
Tries to build a CoinductionKit.
Builtin equality
primEqualityName :: TCM QNameSource
Get the name of the equality type.