Agda-2.2.10: A dependently typed functional programming language and proof assistant Source code Contents Index

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 Term Source

bindBuiltinType1 :: String -> Expr -> TCM () Source

Bind something of type Set -> Set.

bindBuiltinZero' :: String -> TCM Term -> Expr -> TCM Term Source

bindBuiltinSuc' :: String -> TCM Term -> Expr -> TCM Term Source

typeOfSizeInf :: TCM Type Source

typeOfSizeSuc :: TCM Type Source

bindBuiltinNil :: Expr -> TCM Term Source

Built-in nil should have type {A:Set} -> List A

bindBuiltinCons :: Expr -> TCM Term Source

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 Term Source

bindBuiltinDummyConstructor :: Expr -> TCM Term Source

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