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
31
32
33
34
35
36
37
38
39
40
41
type t =
| Proposition
| Any of int
let compare (s1: t) (s2: t): int =
match s1, s2 with
| Proposition, Proposition ->
0
| Proposition, _ ->
-1
| Any i, Any j ->
Stdlib.compare i j
| Any _, Proposition ->
+1
let is_sub (s1: t) (s2: t): bool =
compare s1 s2 <= 0
let is_super (s1: t) (s2: t): bool =
is_sub s2 s1
let type_of (s: t): t =
match s with
| Proposition ->
Any 0
| Any i ->
Any (i + 1)
let pi_sort (arg: t) (res: t): t =
match arg, res with
| _, Proposition ->
Proposition
| Proposition, Any j ->
Any j
| Any i, Any j ->
Any (max i j)