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




Checking builtin pragmas

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

Bind something of type Set -> Set.

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

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.