blob: cf07a4b61c99a71f8cd109f6cb624d0eb54c3936 (
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
|
open Bwd
type value =
| Neutral of ne
| Pi of value * clos
| Lam of clos
| Sg of value * clos
| Pair of value * value
| Type
| Bool
| True
| False
and ne = ne_head * frame bwd
and ne_head = Var of int (* De Bruijn levels *)
and frame =
| BoolElim of {
cmot: clos;
vtrue: value;
vfalse: value;
}
| App of value
| Fst
| Snd
and env = value bwd
and clos = Clos of { body : Syntax.tm; env : env }
|