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

Agda.TypeChecking.Rules.Builtin

Contents Checking builtin pragmas

Synopsis

ensureInductive :: Term -> TCM () bindBuiltinType :: String -> Expr -> TCM () bindBuiltinBool :: String -> Expr -> TCM () bindBuiltinType1 :: String -> Expr -> TCM () bindBuiltinZero :: Expr -> TCM () bindBuiltinSuc :: Expr -> TCM () typeOfSizeInf :: TCM Type typeOfSizeSuc :: TCM Type bindBuiltinNil :: Expr -> TCM () bindBuiltinCons :: Expr -> TCM () bindBuiltinPrimitive :: String -> String -> Expr -> (Term -> TCM ()) -> TCM () builtinPrimitives :: [(String, (String, Term -> TCM ()))] builtinConstructors :: [(String, Expr -> TCM ())] builtinPostulates :: [(String, TCM Type)] bindConstructor :: String -> (Expr -> TCM ()) -> Expr -> TCM () bindPostulate :: String -> TCM Type -> Expr -> TCM () bindBuiltin :: String -> Expr -> TCM ()

Checking builtin pragmas

ensureInductive :: Term -> TCM () Source

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

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

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

Bind something of type Set -> Set.

bindBuiltinZero :: Expr -> TCM () Source

bindBuiltinSuc :: Expr -> TCM () Source

typeOfSizeInf :: TCM Type Source

typeOfSizeSuc :: TCM Type Source

bindBuiltinNil :: Expr -> TCM () Source

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

bindBuiltinCons :: Expr -> TCM () 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

builtinConstructors :: [(String, Expr -> TCM ())] Source

Builtin constructors

builtinPostulates :: [(String, TCM Type)] Source

Builtin postulates

bindConstructor :: String -> (Expr -> TCM ()) -> 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.4.2