blob: 6f5e11c4947a37a25e47cfeefb277dc93f72cea6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
|
open Bwd
type t = Data.value =
| Neutral of ne
| Pi of Ident.local * t * clo
| Lam of Ident.local * clo
| Sg of Ident.local * t * clo
| Pair of t * t
| Type
| Bool
| True
| False
and ne = Data.ne
and ne_head = Data.ne_head = Var of int (* De Bruijn levels *)
and frm = Data.frm =
| App of t
| Fst
| Snd
| BoolElim of {
motive_var : Ident.local;
motive : clo;
true_case : t;
false_case: t;
}
and env = Data.env
and clo = Data.clo = Clo of { body : Data.syn; env : env }
let var i = Neutral (Var i, Bwd.Emp)
|