mirror of
https://github.com/HigherOrderCO/Kind.git
synced 2024-07-07 10:06:36 +03:00
85ad65b026
Now, there are two local binders: let x = ... use x = ... The 'let' binder will create a local definition, type-check it, and assign a name to it. When compiled, it will create 'dup' nodes. The 'use' binder is just an alias. It will not bind a new variable, and, when compiled, will create inline copies. Also, for type-checking, it allows creating aliases that are definitionaly equal for the checker.
14 lines
578 B
Plaintext
14 lines
578 B
Plaintext
// exp : ∀(n: Nat) Nat = λn λm λP λs λz (m ∀(x:P)P (n P))
|
|
T_EXP = (Kind.all "n" _Nat λn(Kind.all "m" _Nat λm(_Nat)))
|
|
T_exp = (Kind.lam "n" λn(Kind.lam "m" λm(Kind.lam "P" λP(Kind.app (Kind.app m (Kind.all "x" P λx(P))) (Kind.app n P)))))
|
|
|
|
// C2 : Nat = λs λz (s (s z))
|
|
T_C2 = _Nat
|
|
T_c2 = (Kind.lam "P" λP(Kind.lam "s" λs(Kind.lam "z" λz(Kind.app s (Kind.app s z)))))
|
|
|
|
// Checks if (work 2^4) is propositionally equal to true
|
|
test10
|
|
: String
|
|
= use term = (Kind.app (Kind.app T_exp T_c2) T_c2)
|
|
(Kind.Term.show (Kind.normal Bool.true term Nat.zero) Nat.zero)
|