Agda-2.2.10: A dependently typed functional programming language and proof assistant

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)]

inductiveCheck :: String -> Term -> TCM ()

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

bindBuiltinBool :: String -> Expr -> TCM Term

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

Bind something of type `Set -> Set`.

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

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

typeOfSizeInf :: TCM Type

typeOfSizeSuc :: TCM Type

bindBuiltinNil :: Expr -> TCM Term

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

bindBuiltinCons :: Expr -> TCM Term

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

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 ()

`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)]

Builtin constructors

builtinPostulates :: [(String, TCM Type)]

Builtin postulates

bindConstructor :: String -> (Expr -> TCM Term) -> Expr -> TCM ()

Bind a builtin constructor. Pre-condition: argument is an element of `builtinConstructors`.

bindPostulate :: String -> TCM Type -> Expr -> TCM ()

Bind a builtin postulate. Pre-condition: argument is an element of `builtinPostulates`.

bindBuiltin :: String -> Expr -> TCM ()

Bind a builtin thing to an expression.