1 | open Preamble |
---|
2 | |
---|
3 | open Hints_declaration |
---|
4 | |
---|
5 | open Core_notation |
---|
6 | |
---|
7 | open Pts |
---|
8 | |
---|
9 | open Logic |
---|
10 | |
---|
11 | open Relations |
---|
12 | |
---|
13 | type bool = |
---|
14 | | True |
---|
15 | | False |
---|
16 | |
---|
17 | (** val bool_rect_Type4 : 'a1 -> 'a1 -> bool -> 'a1 **) |
---|
18 | let rec bool_rect_Type4 h_true h_false = function |
---|
19 | | True -> h_true |
---|
20 | | False -> h_false |
---|
21 | |
---|
22 | (** val bool_rect_Type5 : 'a1 -> 'a1 -> bool -> 'a1 **) |
---|
23 | let rec bool_rect_Type5 h_true h_false = function |
---|
24 | | True -> h_true |
---|
25 | | False -> h_false |
---|
26 | |
---|
27 | (** val bool_rect_Type3 : 'a1 -> 'a1 -> bool -> 'a1 **) |
---|
28 | let rec bool_rect_Type3 h_true h_false = function |
---|
29 | | True -> h_true |
---|
30 | | False -> h_false |
---|
31 | |
---|
32 | (** val bool_rect_Type2 : 'a1 -> 'a1 -> bool -> 'a1 **) |
---|
33 | let rec bool_rect_Type2 h_true h_false = function |
---|
34 | | True -> h_true |
---|
35 | | False -> h_false |
---|
36 | |
---|
37 | (** val bool_rect_Type1 : 'a1 -> 'a1 -> bool -> 'a1 **) |
---|
38 | let rec bool_rect_Type1 h_true h_false = function |
---|
39 | | True -> h_true |
---|
40 | | False -> h_false |
---|
41 | |
---|
42 | (** val bool_rect_Type0 : 'a1 -> 'a1 -> bool -> 'a1 **) |
---|
43 | let rec bool_rect_Type0 h_true h_false = function |
---|
44 | | True -> h_true |
---|
45 | | False -> h_false |
---|
46 | |
---|
47 | (** val bool_inv_rect_Type4 : bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) |
---|
48 | let bool_inv_rect_Type4 hterm h1 h2 = |
---|
49 | let hcut = bool_rect_Type4 h1 h2 hterm in hcut __ |
---|
50 | |
---|
51 | (** val bool_inv_rect_Type3 : bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) |
---|
52 | let bool_inv_rect_Type3 hterm h1 h2 = |
---|
53 | let hcut = bool_rect_Type3 h1 h2 hterm in hcut __ |
---|
54 | |
---|
55 | (** val bool_inv_rect_Type2 : bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) |
---|
56 | let bool_inv_rect_Type2 hterm h1 h2 = |
---|
57 | let hcut = bool_rect_Type2 h1 h2 hterm in hcut __ |
---|
58 | |
---|
59 | (** val bool_inv_rect_Type1 : bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) |
---|
60 | let bool_inv_rect_Type1 hterm h1 h2 = |
---|
61 | let hcut = bool_rect_Type1 h1 h2 hterm in hcut __ |
---|
62 | |
---|
63 | (** val bool_inv_rect_Type0 : bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) |
---|
64 | let bool_inv_rect_Type0 hterm h1 h2 = |
---|
65 | let hcut = bool_rect_Type0 h1 h2 hterm in hcut __ |
---|
66 | |
---|
67 | (** val bool_discr : bool -> bool -> __ **) |
---|
68 | let bool_discr x y = |
---|
69 | Logic.eq_rect_Type2 x |
---|
70 | (match x with |
---|
71 | | True -> Obj.magic (fun _ dH -> dH) |
---|
72 | | False -> Obj.magic (fun _ dH -> dH)) y |
---|
73 | |
---|
74 | (** val notb : bool -> bool **) |
---|
75 | let notb = function |
---|
76 | | True -> False |
---|
77 | | False -> True |
---|
78 | |
---|
79 | (** val andb : bool -> bool -> bool **) |
---|
80 | let andb b1 b2 = |
---|
81 | match b1 with |
---|
82 | | True -> b2 |
---|
83 | | False -> False |
---|
84 | |
---|
85 | (** val orb : bool -> bool -> bool **) |
---|
86 | let orb b1 b2 = |
---|
87 | match b1 with |
---|
88 | | True -> True |
---|
89 | | False -> b2 |
---|
90 | |
---|
91 | (** val xorb : bool -> bool -> bool **) |
---|
92 | let xorb b1 b2 = |
---|
93 | match b1 with |
---|
94 | | True -> |
---|
95 | (match b2 with |
---|
96 | | True -> False |
---|
97 | | False -> True) |
---|
98 | | False -> |
---|
99 | (match b2 with |
---|
100 | | True -> True |
---|
101 | | False -> False) |
---|
102 | |
---|