blob: 5de5281cdfa1e5a366cf91ee5e8d599e788a5c77 (
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 Ident.t * Data.value Lazy.t
| Pi of Ident.local * t * (* BINDS *) t
| Lam of Ident.local * (* BINDS *) t
| App of t * t
| Sg of Ident.local * t * (* BINDS *) t
| Pair of t * t
| Fst of t
| Snd of t
| Type
| Bool
| True
| False
| BoolElim of {
motive_var : Ident.local;
motive : (* BINDS *) t;
true_case : t;
false_case : t;
scrut : t;
}
|