blob: 859102a750fce408b3ea3918e3552887d19b714f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
type t = Data.syn =
| Var of int
| Def of Name.t * Data.value Lazy.t
| Pi of Name.local * t * (* BINDS *) t
| Lam of Name.local * (* BINDS *) t
| App of t * t
| Sg of Name.local * t * (* BINDS *) t
| Pair of t * t
| Fst of t
| Snd of t
| Type
| Bool
| True
| False
| BoolElim of {
motive_var : Name.local;
motive : (* BINDS *) t;
true_case : t;
false_case : t;
scrut : t;
}
|