1 | open Preamble |
---|
2 | |
---|
3 | open Hints_declaration |
---|
4 | |
---|
5 | open Core_notation |
---|
6 | |
---|
7 | open Pts |
---|
8 | |
---|
9 | open Logic |
---|
10 | |
---|
11 | open Types |
---|
12 | |
---|
13 | open Relations |
---|
14 | |
---|
15 | open Bool |
---|
16 | |
---|
17 | type deqSet = |
---|
18 | __ -> __ -> Bool.bool |
---|
19 | (* singleton inductive, whose constructor was mk_DeqSet *) |
---|
20 | |
---|
21 | (** val deqSet_rect_Type4 : |
---|
22 | (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **) |
---|
23 | let rec deqSet_rect_Type4 h_mk_DeqSet x_3083 = |
---|
24 | let eqb = x_3083 in h_mk_DeqSet __ eqb __ |
---|
25 | |
---|
26 | (** val deqSet_rect_Type5 : |
---|
27 | (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **) |
---|
28 | let rec deqSet_rect_Type5 h_mk_DeqSet x_3085 = |
---|
29 | let eqb = x_3085 in h_mk_DeqSet __ eqb __ |
---|
30 | |
---|
31 | (** val deqSet_rect_Type3 : |
---|
32 | (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **) |
---|
33 | let rec deqSet_rect_Type3 h_mk_DeqSet x_3087 = |
---|
34 | let eqb = x_3087 in h_mk_DeqSet __ eqb __ |
---|
35 | |
---|
36 | (** val deqSet_rect_Type2 : |
---|
37 | (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **) |
---|
38 | let rec deqSet_rect_Type2 h_mk_DeqSet x_3089 = |
---|
39 | let eqb = x_3089 in h_mk_DeqSet __ eqb __ |
---|
40 | |
---|
41 | (** val deqSet_rect_Type1 : |
---|
42 | (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **) |
---|
43 | let rec deqSet_rect_Type1 h_mk_DeqSet x_3091 = |
---|
44 | let eqb = x_3091 in h_mk_DeqSet __ eqb __ |
---|
45 | |
---|
46 | (** val deqSet_rect_Type0 : |
---|
47 | (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **) |
---|
48 | let rec deqSet_rect_Type0 h_mk_DeqSet x_3093 = |
---|
49 | let eqb = x_3093 in h_mk_DeqSet __ eqb __ |
---|
50 | |
---|
51 | type carr = __ |
---|
52 | |
---|
53 | (** val eqb : deqSet -> __ -> __ -> Bool.bool **) |
---|
54 | let rec eqb xxx = |
---|
55 | let yyy = xxx in yyy |
---|
56 | |
---|
57 | (** val deqSet_inv_rect_Type4 : |
---|
58 | deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1 **) |
---|
59 | let deqSet_inv_rect_Type4 hterm h1 = |
---|
60 | let hcut = deqSet_rect_Type4 h1 hterm in hcut __ |
---|
61 | |
---|
62 | (** val deqSet_inv_rect_Type3 : |
---|
63 | deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1 **) |
---|
64 | let deqSet_inv_rect_Type3 hterm h1 = |
---|
65 | let hcut = deqSet_rect_Type3 h1 hterm in hcut __ |
---|
66 | |
---|
67 | (** val deqSet_inv_rect_Type2 : |
---|
68 | deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1 **) |
---|
69 | let deqSet_inv_rect_Type2 hterm h1 = |
---|
70 | let hcut = deqSet_rect_Type2 h1 hterm in hcut __ |
---|
71 | |
---|
72 | (** val deqSet_inv_rect_Type1 : |
---|
73 | deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1 **) |
---|
74 | let deqSet_inv_rect_Type1 hterm h1 = |
---|
75 | let hcut = deqSet_rect_Type1 h1 hterm in hcut __ |
---|
76 | |
---|
77 | (** val deqSet_inv_rect_Type0 : |
---|
78 | deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1 **) |
---|
79 | let deqSet_inv_rect_Type0 hterm h1 = |
---|
80 | let hcut = deqSet_rect_Type0 h1 hterm in hcut __ |
---|
81 | |
---|
82 | (** val beqb : Bool.bool -> Bool.bool -> Bool.bool **) |
---|
83 | let beqb b1 b2 = |
---|
84 | match b1 with |
---|
85 | | Bool.True -> b2 |
---|
86 | | Bool.False -> Bool.notb b2 |
---|
87 | |
---|
88 | (** val deqBool : deqSet **) |
---|
89 | let deqBool = |
---|
90 | Obj.magic beqb |
---|
91 | |
---|
92 | (** val eq_option : |
---|
93 | deqSet -> __ Types.option -> __ Types.option -> Bool.bool **) |
---|
94 | let eq_option a a1 a2 = |
---|
95 | match a1 with |
---|
96 | | Types.None -> |
---|
97 | (match a2 with |
---|
98 | | Types.None -> Bool.True |
---|
99 | | Types.Some x -> Bool.False) |
---|
100 | | Types.Some a1' -> |
---|
101 | (match a2 with |
---|
102 | | Types.None -> Bool.False |
---|
103 | | Types.Some a2' -> eqb a a1' a2') |
---|
104 | |
---|
105 | (** val deqOption : deqSet -> deqSet **) |
---|
106 | let deqOption a = |
---|
107 | Obj.magic (eq_option a) |
---|
108 | |
---|
109 | (** val eq_pairs : |
---|
110 | deqSet -> deqSet -> (__, __) Types.prod -> (__, __) Types.prod -> |
---|
111 | Bool.bool **) |
---|
112 | let eq_pairs a b p1 p2 = |
---|
113 | Bool.andb (eqb a p1.Types.fst p2.Types.fst) |
---|
114 | (eqb b p1.Types.snd p2.Types.snd) |
---|
115 | |
---|
116 | (** val deqProd : deqSet -> deqSet -> deqSet **) |
---|
117 | let deqProd a b = |
---|
118 | Obj.magic (eq_pairs a b) |
---|
119 | |
---|
120 | (** val eq_sum : |
---|
121 | deqSet -> deqSet -> (__, __) Types.sum -> (__, __) Types.sum -> Bool.bool **) |
---|
122 | let eq_sum a b p1 p2 = |
---|
123 | match p1 with |
---|
124 | | Types.Inl a1 -> |
---|
125 | (match p2 with |
---|
126 | | Types.Inl a2 -> eqb a a1 a2 |
---|
127 | | Types.Inr b2 -> Bool.False) |
---|
128 | | Types.Inr b1 -> |
---|
129 | (match p2 with |
---|
130 | | Types.Inl a2 -> Bool.False |
---|
131 | | Types.Inr b2 -> eqb b b1 b2) |
---|
132 | |
---|
133 | (** val deqSum : deqSet -> deqSet -> deqSet **) |
---|
134 | let deqSum a b = |
---|
135 | Obj.magic (eq_sum a b) |
---|
136 | |
---|
137 | (** val eq_sigma : deqSet -> __ Types.sig0 -> __ Types.sig0 -> Bool.bool **) |
---|
138 | let eq_sigma a p1 p2 = |
---|
139 | let a1 = p1 in let a2 = p2 in eqb a a1 a2 |
---|
140 | |
---|
141 | (** val deqSig : deqSet -> deqSet **) |
---|
142 | let deqSig a = |
---|
143 | Obj.magic (eq_sigma a) |
---|
144 | |
---|