19 (* singleton inductive, whose constructor was mk_DeqSet *)
21 (** val deqSet_rect_Type4 :
22 (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **)
23 let rec deqSet_rect_Type4 h_mk_DeqSet x_3369 =
24 let eqb = x_3369 in h_mk_DeqSet __ eqb __
26 (** val deqSet_rect_Type5 :
27 (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **)
28 let rec deqSet_rect_Type5 h_mk_DeqSet x_3371 =
29 let eqb = x_3371 in h_mk_DeqSet __ eqb __
31 (** val deqSet_rect_Type3 :
32 (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **)
33 let rec deqSet_rect_Type3 h_mk_DeqSet x_3373 =
34 let eqb = x_3373 in h_mk_DeqSet __ eqb __
36 (** val deqSet_rect_Type2 :
37 (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **)
38 let rec deqSet_rect_Type2 h_mk_DeqSet x_3375 =
39 let eqb = x_3375 in h_mk_DeqSet __ eqb __
41 (** val deqSet_rect_Type1 :
42 (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **)
43 let rec deqSet_rect_Type1 h_mk_DeqSet x_3377 =
44 let eqb = x_3377 in h_mk_DeqSet __ eqb __
46 (** val deqSet_rect_Type0 :
47 (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **)
48 let rec deqSet_rect_Type0 h_mk_DeqSet x_3379 =
49 let eqb = x_3379 in h_mk_DeqSet __ eqb __
53 (** val eqb : deqSet -> __ -> __ -> Bool.bool **)
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 __
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 __
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 __
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 __
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 __
82 (** val beqb : Bool.bool -> Bool.bool -> Bool.bool **)
86 | Bool.False -> Bool.notb b2
88 (** val deqBool : deqSet **)
93 deqSet -> __ Types.option -> __ Types.option -> Bool.bool **)
94 let eq_option a a1 a2 =
98 | Types.None -> Bool.True
99 | Types.Some x -> Bool.False)
102 | Types.None -> Bool.False
103 | Types.Some a2' -> eqb a a1' a2')
105 (** val deqOption : deqSet -> deqSet **)
107 Obj.magic (eq_option a)
110 deqSet -> deqSet -> (__, __) Types.prod -> (__, __) Types.prod ->
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)
116 (** val deqProd : deqSet -> deqSet -> deqSet **)
118 Obj.magic (eq_pairs a b)
121 deqSet -> deqSet -> (__, __) Types.sum -> (__, __) Types.sum -> Bool.bool **)
122 let eq_sum a b p1 p2 =
126 | Types.Inl a2 -> eqb a a1 a2
127 | Types.Inr b2 -> Bool.False)
130 | Types.Inl a2 -> Bool.False
131 | Types.Inr b2 -> eqb b b1 b2)
133 (** val deqSum : deqSet -> deqSet -> deqSet **)
135 Obj.magic (eq_sum a b)
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
141 (** val deqSig : deqSet -> deqSet **)
143 Obj.magic (eq_sigma a)