22 (Nat.nat -> 'a1) -> (Nat.nat -> 'a2) -> Nat.nat -> Nat.nat -> ('a1, 'a2)
25 { Types.fst = (f (Div_and_mod.div x m)); Types.snd =
26 (g (Div_and_mod.mod0 x m)) }
29 Nat.nat -> (Nat.nat -> Bool.bool) -> 'a1 -> ('a1 -> 'a1 -> 'a1) ->
30 (Nat.nat -> 'a1) -> 'a1 **)
31 let rec bigop n p nil op f =
36 | Bool.True -> op (f k) (bigop k p nil op f)
37 | Bool.False -> bigop k p nil op f)
41 (* singleton inductive, whose constructor was mk_Aop *)
43 (** val aop_rect_Type4 :
44 'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
45 let rec aop_rect_Type4 nil h_mk_Aop x_969 =
46 let op = x_969 in h_mk_Aop op __ __ __
48 (** val aop_rect_Type5 :
49 'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
50 let rec aop_rect_Type5 nil h_mk_Aop x_971 =
51 let op = x_971 in h_mk_Aop op __ __ __
53 (** val aop_rect_Type3 :
54 'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
55 let rec aop_rect_Type3 nil h_mk_Aop x_973 =
56 let op = x_973 in h_mk_Aop op __ __ __
58 (** val aop_rect_Type2 :
59 'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
60 let rec aop_rect_Type2 nil h_mk_Aop x_975 =
61 let op = x_975 in h_mk_Aop op __ __ __
63 (** val aop_rect_Type1 :
64 'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
65 let rec aop_rect_Type1 nil h_mk_Aop x_977 =
66 let op = x_977 in h_mk_Aop op __ __ __
68 (** val aop_rect_Type0 :
69 'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
70 let rec aop_rect_Type0 nil h_mk_Aop x_979 =
71 let op = x_979 in h_mk_Aop op __ __ __
73 (** val op : 'a1 -> 'a1 aop -> 'a1 -> 'a1 -> 'a1 **)
77 (** val aop_inv_rect_Type4 :
78 'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
80 let aop_inv_rect_Type4 x2 hterm h1 =
81 let hcut = aop_rect_Type4 x2 h1 hterm in hcut __
83 (** val aop_inv_rect_Type3 :
84 'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
86 let aop_inv_rect_Type3 x2 hterm h1 =
87 let hcut = aop_rect_Type3 x2 h1 hterm in hcut __
89 (** val aop_inv_rect_Type2 :
90 'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
92 let aop_inv_rect_Type2 x2 hterm h1 =
93 let hcut = aop_rect_Type2 x2 h1 hterm in hcut __
95 (** val aop_inv_rect_Type1 :
96 'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
98 let aop_inv_rect_Type1 x2 hterm h1 =
99 let hcut = aop_rect_Type1 x2 h1 hterm in hcut __
101 (** val aop_inv_rect_Type0 :
102 'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
104 let aop_inv_rect_Type0 x2 hterm h1 =
105 let hcut = aop_rect_Type0 x2 h1 hterm in hcut __
107 (** val aop_discr : 'a1 -> 'a1 aop -> 'a1 aop -> __ **)
108 let aop_discr a2 x y =
109 Logic.eq_rect_Type2 x
110 (let a0 = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y
112 (** val dpi1__o__op :
113 'a1 -> ('a1 aop, 'a2) Types.dPair -> 'a1 -> 'a1 -> 'a1 **)
114 let dpi1__o__op x1 x3 =
119 (* singleton inductive, whose constructor was mk_ACop *)
121 (** val aCop_rect_Type4 :
122 'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2 **)
123 let rec aCop_rect_Type4 nil h_mk_ACop x_997 =
124 let aop0 = x_997 in h_mk_ACop aop0 __
126 (** val aCop_rect_Type5 :
127 'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2 **)
128 let rec aCop_rect_Type5 nil h_mk_ACop x_999 =
129 let aop0 = x_999 in h_mk_ACop aop0 __
131 (** val aCop_rect_Type3 :
132 'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2 **)
133 let rec aCop_rect_Type3 nil h_mk_ACop x_1001 =
134 let aop0 = x_1001 in h_mk_ACop aop0 __
136 (** val aCop_rect_Type2 :
137 'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2 **)
138 let rec aCop_rect_Type2 nil h_mk_ACop x_1003 =
139 let aop0 = x_1003 in h_mk_ACop aop0 __
141 (** val aCop_rect_Type1 :
142 'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2 **)
143 let rec aCop_rect_Type1 nil h_mk_ACop x_1005 =
144 let aop0 = x_1005 in h_mk_ACop aop0 __
146 (** val aCop_rect_Type0 :
147 'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2 **)
148 let rec aCop_rect_Type0 nil h_mk_ACop x_1007 =
149 let aop0 = x_1007 in h_mk_ACop aop0 __
151 (** val aop0 : 'a1 -> 'a1 aCop -> 'a1 aop **)
152 let rec aop0 nil xxx =
155 (** val aCop_inv_rect_Type4 :
156 'a1 -> 'a1 aCop -> ('a1 aop -> __ -> __ -> 'a2) -> 'a2 **)
157 let aCop_inv_rect_Type4 x2 hterm h1 =
158 let hcut = aCop_rect_Type4 x2 h1 hterm in hcut __
160 (** val aCop_inv_rect_Type3 :
161 'a1 -> 'a1 aCop -> ('a1 aop -> __ -> __ -> 'a2) -> 'a2 **)
162 let aCop_inv_rect_Type3 x2 hterm h1 =
163 let hcut = aCop_rect_Type3 x2 h1 hterm in hcut __
165 (** val aCop_inv_rect_Type2 :
166 'a1 -> 'a1 aCop -> ('a1 aop -> __ -> __ -> 'a2) -> 'a2 **)
167 let aCop_inv_rect_Type2 x2 hterm h1 =
168 let hcut = aCop_rect_Type2 x2 h1 hterm in hcut __
170 (** val aCop_inv_rect_Type1 :
171 'a1 -> 'a1 aCop -> ('a1 aop -> __ -> __ -> 'a2) -> 'a2 **)
172 let aCop_inv_rect_Type1 x2 hterm h1 =
173 let hcut = aCop_rect_Type1 x2 h1 hterm in hcut __
175 (** val aCop_inv_rect_Type0 :
176 'a1 -> 'a1 aCop -> ('a1 aop -> __ -> __ -> 'a2) -> 'a2 **)
177 let aCop_inv_rect_Type0 x2 hterm h1 =
178 let hcut = aCop_rect_Type0 x2 h1 hterm in hcut __
180 (** val aCop_discr : 'a1 -> 'a1 aCop -> 'a1 aCop -> __ **)
181 let aCop_discr a2 x y =
182 Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y
184 (** val dpi1__o__aop__o__op :
185 'a1 -> ('a1 aCop, 'a2) Types.dPair -> 'a1 -> 'a1 -> 'a1 **)
186 let dpi1__o__aop__o__op x1 x3 =
187 op x1 (aop0 x1 x3.Types.dpi1)
189 (** val aop__o__op : 'a1 -> 'a1 aCop -> 'a1 -> 'a1 -> 'a1 **)
190 let aop__o__op x1 x2 =
193 (** val dpi1__o__aop : 'a1 -> ('a1 aCop, 'a2) Types.dPair -> 'a1 aop **)
194 let dpi1__o__aop x1 x3 =
195 aop0 x1 x3.Types.dpi1
197 type 'a range = { enum : (Nat.nat -> 'a); upto : Nat.nat;
198 filter : (Nat.nat -> Bool.bool) }
200 (** val range_rect_Type4 :
201 ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1
203 let rec range_rect_Type4 h_mk_range x_1023 =
204 let { enum = enum0; upto = upto0; filter = filter0 } = x_1023 in
205 h_mk_range enum0 upto0 filter0
207 (** val range_rect_Type5 :
208 ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1
210 let rec range_rect_Type5 h_mk_range x_1025 =
211 let { enum = enum0; upto = upto0; filter = filter0 } = x_1025 in
212 h_mk_range enum0 upto0 filter0
214 (** val range_rect_Type3 :
215 ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1
217 let rec range_rect_Type3 h_mk_range x_1027 =
218 let { enum = enum0; upto = upto0; filter = filter0 } = x_1027 in
219 h_mk_range enum0 upto0 filter0
221 (** val range_rect_Type2 :
222 ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1
224 let rec range_rect_Type2 h_mk_range x_1029 =
225 let { enum = enum0; upto = upto0; filter = filter0 } = x_1029 in
226 h_mk_range enum0 upto0 filter0
228 (** val range_rect_Type1 :
229 ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1
231 let rec range_rect_Type1 h_mk_range x_1031 =
232 let { enum = enum0; upto = upto0; filter = filter0 } = x_1031 in
233 h_mk_range enum0 upto0 filter0
235 (** val range_rect_Type0 :
236 ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1
238 let rec range_rect_Type0 h_mk_range x_1033 =
239 let { enum = enum0; upto = upto0; filter = filter0 } = x_1033 in
240 h_mk_range enum0 upto0 filter0
242 (** val enum : 'a1 range -> Nat.nat -> 'a1 **)
246 (** val upto : 'a1 range -> Nat.nat **)
250 (** val filter : 'a1 range -> Nat.nat -> Bool.bool **)
254 (** val range_inv_rect_Type4 :
255 'a1 range -> ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> __
257 let range_inv_rect_Type4 hterm h1 =
258 let hcut = range_rect_Type4 h1 hterm in hcut __
260 (** val range_inv_rect_Type3 :
261 'a1 range -> ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> __
263 let range_inv_rect_Type3 hterm h1 =
264 let hcut = range_rect_Type3 h1 hterm in hcut __
266 (** val range_inv_rect_Type2 :
267 'a1 range -> ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> __
269 let range_inv_rect_Type2 hterm h1 =
270 let hcut = range_rect_Type2 h1 hterm in hcut __
272 (** val range_inv_rect_Type1 :
273 'a1 range -> ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> __
275 let range_inv_rect_Type1 hterm h1 =
276 let hcut = range_rect_Type1 h1 hterm in hcut __
278 (** val range_inv_rect_Type0 :
279 'a1 range -> ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> __
281 let range_inv_rect_Type0 hterm h1 =
282 let hcut = range_rect_Type0 h1 hterm in hcut __
284 (** val range_discr : 'a1 range -> 'a1 range -> __ **)
285 let range_discr x y =
286 Logic.eq_rect_Type2 x
287 (let { enum = a0; upto = a10; filter = a2 } = x in
288 Obj.magic (fun _ dH -> dH __ __ __)) y
290 type 'a dop = { sum0 : 'a aCop; prod0 : ('a -> 'a -> 'a) }
292 (** val dop_rect_Type4 :
293 'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
295 let rec dop_rect_Type4 nil h_mk_Dop x_1051 =
296 let { sum0 = sum1; prod0 = prod1 } = x_1051 in h_mk_Dop sum1 prod1 __ __
298 (** val dop_rect_Type5 :
299 'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
301 let rec dop_rect_Type5 nil h_mk_Dop x_1053 =
302 let { sum0 = sum1; prod0 = prod1 } = x_1053 in h_mk_Dop sum1 prod1 __ __
304 (** val dop_rect_Type3 :
305 'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
307 let rec dop_rect_Type3 nil h_mk_Dop x_1055 =
308 let { sum0 = sum1; prod0 = prod1 } = x_1055 in h_mk_Dop sum1 prod1 __ __
310 (** val dop_rect_Type2 :
311 'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
313 let rec dop_rect_Type2 nil h_mk_Dop x_1057 =
314 let { sum0 = sum1; prod0 = prod1 } = x_1057 in h_mk_Dop sum1 prod1 __ __
316 (** val dop_rect_Type1 :
317 'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
319 let rec dop_rect_Type1 nil h_mk_Dop x_1059 =
320 let { sum0 = sum1; prod0 = prod1 } = x_1059 in h_mk_Dop sum1 prod1 __ __
322 (** val dop_rect_Type0 :
323 'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
325 let rec dop_rect_Type0 nil h_mk_Dop x_1061 =
326 let { sum0 = sum1; prod0 = prod1 } = x_1061 in h_mk_Dop sum1 prod1 __ __
328 (** val sum0 : 'a1 -> 'a1 dop -> 'a1 aCop **)
329 let rec sum0 nil xxx =
332 (** val prod0 : 'a1 -> 'a1 dop -> 'a1 -> 'a1 -> 'a1 **)
333 let rec prod0 nil xxx =
336 (** val dop_inv_rect_Type4 :
337 'a1 -> 'a1 dop -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ ->
339 let dop_inv_rect_Type4 x2 hterm h1 =
340 let hcut = dop_rect_Type4 x2 h1 hterm in hcut __
342 (** val dop_inv_rect_Type3 :
343 'a1 -> 'a1 dop -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ ->
345 let dop_inv_rect_Type3 x2 hterm h1 =
346 let hcut = dop_rect_Type3 x2 h1 hterm in hcut __
348 (** val dop_inv_rect_Type2 :
349 'a1 -> 'a1 dop -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ ->
351 let dop_inv_rect_Type2 x2 hterm h1 =
352 let hcut = dop_rect_Type2 x2 h1 hterm in hcut __
354 (** val dop_inv_rect_Type1 :
355 'a1 -> 'a1 dop -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ ->
357 let dop_inv_rect_Type1 x2 hterm h1 =
358 let hcut = dop_rect_Type1 x2 h1 hterm in hcut __
360 (** val dop_inv_rect_Type0 :
361 'a1 -> 'a1 dop -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ ->
363 let dop_inv_rect_Type0 x2 hterm h1 =
364 let hcut = dop_rect_Type0 x2 h1 hterm in hcut __
366 (** val dop_discr : 'a1 -> 'a1 dop -> 'a1 dop -> __ **)
367 let dop_discr a2 x y =
368 Logic.eq_rect_Type2 x
369 (let { sum0 = a0; prod0 = a10 } = x in
370 Obj.magic (fun _ dH -> dH __ __ __ __)) y