Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.TypeChecking.Rules.Builtin
Contents
Checking builtin pragmas
Synopsis
builtinDatatypes :: [(String, Int)]
inductiveCheck :: String -> Term -> TCM ()
bindBuiltinType :: String -> Expr -> TCM ()
bindBuiltinBool :: String -> Expr -> TCM Term
bindBuiltinType1 :: String -> Expr -> TCM ()
bindBuiltinZero' :: String -> TCM Term -> Expr -> TCM Term
bindBuiltinSuc' :: String -> TCM Term -> Expr -> TCM Term
typeOfSizeInf :: TCM Type
typeOfSizeSuc :: TCM Type
bindBuiltinNil :: Expr -> TCM Term
bindBuiltinCons :: Expr -> TCM Term
bindBuiltinPrimitive :: String -> String -> Expr -> (Term -> TCM ()) -> TCM ()
builtinPrimitives :: [(String, (String, Term -> TCM ()))]
bindBuiltinEquality :: Expr -> TCM ()
bindBuiltinRefl :: Expr -> TCM Term
bindBuiltinDummyConstructor :: Expr -> TCM Term
bindPostulatedName :: String -> Expr -> (QName -> Definition -> TCM Term) -> TCM ()
builtinConstructors :: [(String, Expr -> TCM Term)]
builtinPostulates :: [(String, TCM Type)]
bindConstructor :: String -> (Expr -> TCM Term) -> Expr -> TCM ()
bindPostulate :: String -> TCM Type -> Expr -> TCM ()
bindBuiltin :: String -> Expr -> TCM ()
Checking builtin pragmas
builtinDatatypes :: [(String, Int)]Source
inductiveCheck :: String -> Term -> TCM ()Source
bindBuiltinType :: String -> Expr -> TCM ()Source
bindBuiltinBool :: String -> Expr -> TCM TermSource
bindBuiltinType1 :: String -> Expr -> TCM ()Source
Bind something of type Set -> Set.
bindBuiltinZero' :: String -> TCM Term -> Expr -> TCM TermSource
bindBuiltinSuc' :: String -> TCM Term -> Expr -> TCM TermSource
typeOfSizeInf :: TCM TypeSource
typeOfSizeSuc :: TCM TypeSource
bindBuiltinNil :: Expr -> TCM TermSource
Built-in nil should have type {A:Set} -> List A
bindBuiltinCons :: Expr -> TCM TermSource
Built-in cons should have type {A:Set} -> A -> List A -> List A
bindBuiltinPrimitive :: String -> String -> Expr -> (Term -> TCM ()) -> TCM ()Source
builtinPrimitives :: [(String, (String, Term -> TCM ()))]Source
bindBuiltinEquality :: Expr -> TCM ()Source
bindBuiltinRefl :: Expr -> TCM TermSource
bindBuiltinDummyConstructor :: Expr -> TCM TermSource
bindPostulatedName :: String -> Expr -> (QName -> Definition -> TCM Term) -> TCM ()Source
bindPostulatedName builtin e m checks that e is a postulated name q, and binds the builtin builtin to the term m q def, where def is the current Definition of q.
builtinConstructors :: [(String, Expr -> TCM Term)]Source
Builtin constructors
builtinPostulates :: [(String, TCM Type)]Source
Builtin postulates
bindConstructor :: String -> (Expr -> TCM Term) -> Expr -> TCM ()Source
Bind a builtin constructor. Pre-condition: argument is an element of builtinConstructors.
bindPostulate :: String -> TCM Type -> Expr -> TCM ()Source
Bind a builtin postulate. Pre-condition: argument is an element of builtinPostulates.
bindBuiltin :: String -> Expr -> TCM ()Source
Bind a builtin thing to an expression.
Produced by Haddock version 2.6.1