6.2.901.900
1 Curnel Forms
Curnel forms are the core forms provided cur.
These forms come directly from the trusted core and are all that remain after macro expansion.
TODO: Link to guide regarding macro expansion
The core of cur is essentially TT.
For a very understandable in-depth look at TT, see chapter 2 of
Practical Implementation of a Dependently Typed Functional Programming Language, by
Edwin C. Brady.
Define the universe of types at level n, where n is any natural number.
A synonym for (Type 0).
(lambda (id : type-expr) body-expr)
|
| (λ (id : type-expr) body-expr) |
Produces a single arity procedure, binding the identifier id of type type-expr in body-expr and in the type of
body-expr.
Both type-expr and body-expr can contain non-curnel forms, such as macros.
Currently, Cur will return the underlying representation of a procedure when a lambda is
evaluated at the top-level. Do not rely on this representation.
Example: |
| > (lambda (x : Type) x) | '(λ (x : (Unv 0)) x) |
|
Example: |
| > (λ (x : Type) (lambda (y : x) y)) | '(λ (x : (Unv 0)) (λ (y : x) y)) |
|
(#%app procedure argument)
|
Applies the single arity procedure to argument.
Example: |
| > ((lambda (x : (Type 1)) x) Type) | '(Unv 0) |
|
Example: |
| > (#%app (lambda (x : (Type 1)) x) Type) | '(Unv 0) |
|
(forall (id : type-expr) body-expr)
|
| (∀ (id : type-expr) body-expr) |
Produces a dependent function type, binding the identifier id of type type-expr in body-expr.
Example: |
| > (forall (x : Type) Type) | '(Π (x : (Unv 0)) (Unv 0)) |
|
Example: |
| > (lambda (x : (forall (x : (Type 1)) Type)) | | (x Type)) |
| '(λ (x : (Π (x : (Unv 1)) (Unv 0))) (x (Unv 0))) |
|
(data id : type-expr (id* : type-expr*) ...)
|
Defines an inductive datatype named id of type type-expr, with constructors
id* each with the corresponding type type-expr*.
Currently, Cur does not attempt to ensure the well-foundedness of the inductive definition.
For instance, Cur does not currently perform strict positivity checking.
Examples: |
| > (data Bool : Type | | (true : Bool) | | (false : Bool)) |
| | > ((lambda (x : Bool) x) true) | 'true | | > (data False : Type) | | > (data And : (forall (A : Type) (forall (B : Type) Type)) | | (conj : (forall (A : Type) (forall (B : Type) (forall (a : A) (forall (b : B) ((And A) B))))))) |
| | > ((((conj Bool) Bool) true) false) | '((((conj Bool) Bool) true) false) |
|
(elim type motive-universe)
|
Returns the inductive eliminator for type where the motive-universe is the universe
of the motive.
The eliminator expects the next argument to be the motive, the next N arguments to be the methods for
each of the N constructors of the inductive type type, the next P arguments
to be the parameters p_0 ... p_P of the inductive type, and the final argument to be the term to
eliminate of type (type p_0 ... p_P).
The following example runs (sub1 (s z)).
Examples: |
| > (data Nat : Type | | (z : Nat) | | (s : (forall (n : Nat) Nat))) |
| | > (((((elim Nat Type) | | (lambda (x : Nat) Nat)) | | z) | | (lambda (n : Nat) (lambda (IH : Nat) n))) | | (s z)) |
| 'z |
|
Binds id to the result of expr.
Examples: |
| > (data Nat : Type | | (z : Nat) | | (s : (forall (n : Nat) Nat))) |
| | > (define sub1 (lambda (n : Nat) | | (((((elim Nat Type) (lambda (x : Nat) Nat)) | | z) | | (lambda (n : Nat) (lambda (IH : Nat) n))) n))) |
| | > (sub1 (s (s z))) | '(s z) | | > (sub1 (s z)) | 'z | | > (sub1 z) | 'z |
|
TODO: Document require and provide