mirror of
https://github.com/HigherOrderCO/Kind.git
synced 2024-09-11 19:47:15 +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.
33 lines
669 B
Plaintext
33 lines
669 B
Plaintext
Kind
|
|
: String
|
|
= use a = (Kind.lam
|
|
"f"
|
|
λf (Kind.lam "x" λx (Kind.app f (Kind.app f x)))
|
|
)
|
|
use b = (Kind.lam
|
|
"f"
|
|
λf (Kind.lam "x" λx (Kind.app f (Kind.app f x)))
|
|
)
|
|
use Test = (Kind.all
|
|
"A"
|
|
Kind.set
|
|
λA
|
|
(Kind.all
|
|
"B"
|
|
Kind.set
|
|
λB (Kind.all "a" A λa (Kind.all "b" B λb B))
|
|
)
|
|
)
|
|
use test = (Kind.lam
|
|
"A"
|
|
λA
|
|
(Kind.lam
|
|
"B"
|
|
λB (Kind.lam "a" λa (Kind.lam "b" λb b))
|
|
)
|
|
)
|
|
use P = λx String
|
|
use some = λvalue (Kind.Term.show value Nat.zero)
|
|
use none = "error"
|
|
use chk = (Kind.check test Test Nat.zero)
|
|
(~chk P some none) |