|
Agda.TypeChecking.Rules.Builtin |
|
|
|
|
|
Synopsis |
|
|
|
|
Checking builtin pragmas
|
|
|
|
|
|
|
|
|
|
|
Bind something of type Set -> Set.
|
|
|
|
|
|
|
|
|
|
|
Built-in nil should have type {A:Set} -> List A
|
|
|
Built-in cons should have type {A:Set} -> A -> List A -> List A
|
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
Builtin constructors
|
|
|
Builtin postulates
|
|
|
Bind a builtin constructor. Pre-condition: argument is an element of
builtinConstructors.
|
|
|
Bind a builtin postulate. Pre-condition: argument is an element of
builtinPostulates.
|
|
|
Bind a builtin thing to an expression.
|
|
Produced by Haddock version 2.6.1 |