mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-10-26 08:09:22 +03:00
13 lines
448 B
Plaintext
13 lines
448 B
Plaintext
type Term ~ (T: Type) {
|
|
var<A: Type>(val: A) ~ (T = A)
|
|
lam<A: Type, B: Type>(bod: Term(A) -> Term(B)) ~ (T = A -> B)
|
|
app<A: Type, B: Type>(fun: Term(A -> B), arg: Term(A)) ~ (T = B)
|
|
}
|
|
|
|
//data Term : (T : Type) where
|
|
//var : (A : Type) -> (val: A) -> Term A
|
|
//lam : (A B : Type) -> (bod : Term A -> Term B) -> Term (A -> B)
|
|
//app : (A B : Type) -> (fun : Term (A -> B)) -> Term B
|
|
|
|
//Term.foo: T
|