mirror of
https://github.com/HigherOrderCO/Kind.git
synced 2024-10-26 16:20:58 +03:00
d059c82c1f
ADTs can be defined with the syntax: data Vector T (len: Nat) | cons (len: Nat) (head: T) (tail: (Vector T len)) : (Vector T (Nat.succ len)) | nil : (Vector T Nat.zero) Which will convert to the equivalent inductive λ-encoding (via self). Pattern-matching has the syntax: match x = expr with (a: A) (b: B) ... { ctr0: ret0 ctr1: ret1 }: motive The 'with' syntax is used to explicitly move values down the cases, crating lambdas for them. This linearizes them (which avoids cloning) and specializes their type w.r.t. the matched value, for proving. We also allow a shorthand for top-level definitions, as: foo (a: A) (b: B) ... : R = body This will auto-add lambdas before 'body'. If 'body' is a pattern-match, the lambdas will be automatically moved down, so this has the effect of linearizing top-level args, without needing explicit 'with' annotations.
14 lines
420 B
Plaintext
14 lines
420 B
Plaintext
A : * =
|
|
$(self: A)
|
|
∀(P: ∀(x: A) *)
|
|
∀(s: ∀(t: ∀(T: *) ∀(k: ∀(pred: A) T) T) (P (t A A.succ)))
|
|
∀(z: ∀(t: ∀(T: *) ∀(k: T) T) (P (t A A.zero)))
|
|
(P self)
|
|
|
|
//∀(k: ∀(x: X) ∀(y: Y) (P (K x y)))
|
|
//-------------------------------------
|
|
//∀(k: ∀(p: (X,Y)) (P (p λxλy(K x y))))
|
|
//-------------------------------------
|
|
//∀(k: ∀(p: Σ(x:X) Σ(y:Y) ()) (P (p λxλy(K x y))))
|
|
|