11 type void = unit (* empty inductive *)
13 (** val void_rect_Type4 : void -> 'a1 **)
14 let rec void_rect_Type4 x_327 =
15 assert false (* absurd case *)
17 (** val void_rect_Type5 : void -> 'a1 **)
18 let rec void_rect_Type5 x_328 =
19 assert false (* absurd case *)
21 (** val void_rect_Type3 : void -> 'a1 **)
22 let rec void_rect_Type3 x_329 =
23 assert false (* absurd case *)
25 (** val void_rect_Type2 : void -> 'a1 **)
26 let rec void_rect_Type2 x_330 =
27 assert false (* absurd case *)
29 (** val void_rect_Type1 : void -> 'a1 **)
30 let rec void_rect_Type1 x_331 =
31 assert false (* absurd case *)
33 (** val void_rect_Type0 : void -> 'a1 **)
34 let rec void_rect_Type0 x_332 =
35 assert false (* absurd case *)
40 (** val unit_rect_Type4 : 'a1 -> unit0 -> 'a1 **)
41 let rec unit_rect_Type4 h_it = function
44 (** val unit_rect_Type5 : 'a1 -> unit0 -> 'a1 **)
45 let rec unit_rect_Type5 h_it = function
48 (** val unit_rect_Type3 : 'a1 -> unit0 -> 'a1 **)
49 let rec unit_rect_Type3 h_it = function
52 (** val unit_rect_Type2 : 'a1 -> unit0 -> 'a1 **)
53 let rec unit_rect_Type2 h_it = function
56 (** val unit_rect_Type1 : 'a1 -> unit0 -> 'a1 **)
57 let rec unit_rect_Type1 h_it = function
60 (** val unit_rect_Type0 : 'a1 -> unit0 -> 'a1 **)
61 let rec unit_rect_Type0 h_it = function
64 (** val unit_inv_rect_Type4 : unit0 -> (__ -> 'a1) -> 'a1 **)
65 let unit_inv_rect_Type4 hterm h1 =
66 let hcut = unit_rect_Type4 h1 hterm in hcut __
68 (** val unit_inv_rect_Type3 : unit0 -> (__ -> 'a1) -> 'a1 **)
69 let unit_inv_rect_Type3 hterm h1 =
70 let hcut = unit_rect_Type3 h1 hterm in hcut __
72 (** val unit_inv_rect_Type2 : unit0 -> (__ -> 'a1) -> 'a1 **)
73 let unit_inv_rect_Type2 hterm h1 =
74 let hcut = unit_rect_Type2 h1 hterm in hcut __
76 (** val unit_inv_rect_Type1 : unit0 -> (__ -> 'a1) -> 'a1 **)
77 let unit_inv_rect_Type1 hterm h1 =
78 let hcut = unit_rect_Type1 h1 hterm in hcut __
80 (** val unit_inv_rect_Type0 : unit0 -> (__ -> 'a1) -> 'a1 **)
81 let unit_inv_rect_Type0 hterm h1 =
82 let hcut = unit_rect_Type0 h1 hterm in hcut __
84 (** val unit_discr : unit0 -> unit0 -> __ **)
86 Logic.eq_rect_Type2 x (let It = x in Obj.magic (fun _ dH -> dH)) y
92 (** val sum_rect_Type4 :
93 ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3 **)
94 let rec sum_rect_Type4 h_inl h_inr = function
95 | Inl x_371 -> h_inl x_371
96 | Inr x_372 -> h_inr x_372
98 (** val sum_rect_Type5 :
99 ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3 **)
100 let rec sum_rect_Type5 h_inl h_inr = function
101 | Inl x_376 -> h_inl x_376
102 | Inr x_377 -> h_inr x_377
104 (** val sum_rect_Type3 :
105 ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3 **)
106 let rec sum_rect_Type3 h_inl h_inr = function
107 | Inl x_381 -> h_inl x_381
108 | Inr x_382 -> h_inr x_382
110 (** val sum_rect_Type2 :
111 ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3 **)
112 let rec sum_rect_Type2 h_inl h_inr = function
113 | Inl x_386 -> h_inl x_386
114 | Inr x_387 -> h_inr x_387
116 (** val sum_rect_Type1 :
117 ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3 **)
118 let rec sum_rect_Type1 h_inl h_inr = function
119 | Inl x_391 -> h_inl x_391
120 | Inr x_392 -> h_inr x_392
122 (** val sum_rect_Type0 :
123 ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3 **)
124 let rec sum_rect_Type0 h_inl h_inr = function
125 | Inl x_396 -> h_inl x_396
126 | Inr x_397 -> h_inr x_397
128 (** val sum_inv_rect_Type4 :
129 ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3 **)
130 let sum_inv_rect_Type4 hterm h1 h2 =
131 let hcut = sum_rect_Type4 h1 h2 hterm in hcut __
133 (** val sum_inv_rect_Type3 :
134 ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3 **)
135 let sum_inv_rect_Type3 hterm h1 h2 =
136 let hcut = sum_rect_Type3 h1 h2 hterm in hcut __
138 (** val sum_inv_rect_Type2 :
139 ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3 **)
140 let sum_inv_rect_Type2 hterm h1 h2 =
141 let hcut = sum_rect_Type2 h1 h2 hterm in hcut __
143 (** val sum_inv_rect_Type1 :
144 ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3 **)
145 let sum_inv_rect_Type1 hterm h1 h2 =
146 let hcut = sum_rect_Type1 h1 h2 hterm in hcut __
148 (** val sum_inv_rect_Type0 :
149 ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3 **)
150 let sum_inv_rect_Type0 hterm h1 h2 =
151 let hcut = sum_rect_Type0 h1 h2 hterm in hcut __
153 (** val sum_discr : ('a1, 'a2) sum -> ('a1, 'a2) sum -> __ **)
155 Logic.eq_rect_Type2 x
157 | Inl a0 -> Obj.magic (fun _ dH -> dH __)
158 | Inr a0 -> Obj.magic (fun _ dH -> dH __)) y
164 (** val option_rect_Type4 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2 **)
165 let rec option_rect_Type4 h_None h_Some = function
167 | Some x_435 -> h_Some x_435
169 (** val option_rect_Type5 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2 **)
170 let rec option_rect_Type5 h_None h_Some = function
172 | Some x_439 -> h_Some x_439
174 (** val option_rect_Type3 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2 **)
175 let rec option_rect_Type3 h_None h_Some = function
177 | Some x_443 -> h_Some x_443
179 (** val option_rect_Type2 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2 **)
180 let rec option_rect_Type2 h_None h_Some = function
182 | Some x_447 -> h_Some x_447
184 (** val option_rect_Type1 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2 **)
185 let rec option_rect_Type1 h_None h_Some = function
187 | Some x_451 -> h_Some x_451
189 (** val option_rect_Type0 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2 **)
190 let rec option_rect_Type0 h_None h_Some = function
192 | Some x_455 -> h_Some x_455
194 (** val option_inv_rect_Type4 :
195 'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2 **)
196 let option_inv_rect_Type4 hterm h1 h2 =
197 let hcut = option_rect_Type4 h1 h2 hterm in hcut __
199 (** val option_inv_rect_Type3 :
200 'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2 **)
201 let option_inv_rect_Type3 hterm h1 h2 =
202 let hcut = option_rect_Type3 h1 h2 hterm in hcut __
204 (** val option_inv_rect_Type2 :
205 'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2 **)
206 let option_inv_rect_Type2 hterm h1 h2 =
207 let hcut = option_rect_Type2 h1 h2 hterm in hcut __
209 (** val option_inv_rect_Type1 :
210 'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2 **)
211 let option_inv_rect_Type1 hterm h1 h2 =
212 let hcut = option_rect_Type1 h1 h2 hterm in hcut __
214 (** val option_inv_rect_Type0 :
215 'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2 **)
216 let option_inv_rect_Type0 hterm h1 h2 =
217 let hcut = option_rect_Type0 h1 h2 hterm in hcut __
219 (** val option_discr : 'a1 option -> 'a1 option -> __ **)
220 let option_discr x y =
221 Logic.eq_rect_Type2 x
223 | None -> Obj.magic (fun _ dH -> dH)
224 | Some a0 -> Obj.magic (fun _ dH -> dH __)) y
226 (** val option_map : ('a1 -> 'a2) -> 'a1 option -> 'a2 option **)
227 let option_map f = function
229 | Some a -> Some (f a)
231 (** val option_map_def : ('a1 -> 'a2) -> 'a2 -> 'a1 option -> 'a2 **)
232 let option_map_def f d = function
236 (** val refute_none_by_refl :
237 ('a1 -> 'a2) -> 'a1 option -> ('a1 -> __ -> 'a3) -> 'a3 **)
238 let refute_none_by_refl p clearme x =
240 | None -> (fun _ -> assert false (* absurd case *))
241 | Some a -> (fun _ p0 -> p0 a __)) __ x
243 type ('a, 'f) dPair = { dpi1 : 'a; dpi2 : 'f }
245 (** val dPair_rect_Type4 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3 **)
246 let rec dPair_rect_Type4 h_mk_DPair x_484 =
247 let { dpi1 = dpi3; dpi2 = dpi4 } = x_484 in h_mk_DPair dpi3 dpi4
249 (** val dPair_rect_Type5 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3 **)
250 let rec dPair_rect_Type5 h_mk_DPair x_486 =
251 let { dpi1 = dpi3; dpi2 = dpi4 } = x_486 in h_mk_DPair dpi3 dpi4
253 (** val dPair_rect_Type3 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3 **)
254 let rec dPair_rect_Type3 h_mk_DPair x_488 =
255 let { dpi1 = dpi3; dpi2 = dpi4 } = x_488 in h_mk_DPair dpi3 dpi4
257 (** val dPair_rect_Type2 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3 **)
258 let rec dPair_rect_Type2 h_mk_DPair x_490 =
259 let { dpi1 = dpi3; dpi2 = dpi4 } = x_490 in h_mk_DPair dpi3 dpi4
261 (** val dPair_rect_Type1 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3 **)
262 let rec dPair_rect_Type1 h_mk_DPair x_492 =
263 let { dpi1 = dpi3; dpi2 = dpi4 } = x_492 in h_mk_DPair dpi3 dpi4
265 (** val dPair_rect_Type0 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3 **)
266 let rec dPair_rect_Type0 h_mk_DPair x_494 =
267 let { dpi1 = dpi3; dpi2 = dpi4 } = x_494 in h_mk_DPair dpi3 dpi4
269 (** val dpi1 : ('a1, 'a2) dPair -> 'a1 **)
273 (** val dpi2 : ('a1, 'a2) dPair -> 'a2 **)
277 (** val dPair_inv_rect_Type4 :
278 ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
279 let dPair_inv_rect_Type4 hterm h1 =
280 let hcut = dPair_rect_Type4 h1 hterm in hcut __
282 (** val dPair_inv_rect_Type3 :
283 ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
284 let dPair_inv_rect_Type3 hterm h1 =
285 let hcut = dPair_rect_Type3 h1 hterm in hcut __
287 (** val dPair_inv_rect_Type2 :
288 ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
289 let dPair_inv_rect_Type2 hterm h1 =
290 let hcut = dPair_rect_Type2 h1 hterm in hcut __
292 (** val dPair_inv_rect_Type1 :
293 ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
294 let dPair_inv_rect_Type1 hterm h1 =
295 let hcut = dPair_rect_Type1 h1 hterm in hcut __
297 (** val dPair_inv_rect_Type0 :
298 ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
299 let dPair_inv_rect_Type0 hterm h1 =
300 let hcut = dPair_rect_Type0 h1 hterm in hcut __
302 (** val dPair_discr : ('a1, 'a2) dPair -> ('a1, 'a2) dPair -> __ **)
303 let dPair_discr x y =
304 Logic.eq_rect_Type2 x
305 (let { dpi1 = a0; dpi2 = a10 } = x in Obj.magic (fun _ dH -> dH __ __)) y
309 (* singleton inductive, whose constructor was mk_Sig *)
311 (** val sig_rect_Type4 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2 **)
312 let rec sig_rect_Type4 h_mk_Sig x_510 =
313 let pi1 = x_510 in h_mk_Sig pi1 __
315 (** val sig_rect_Type5 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2 **)
316 let rec sig_rect_Type5 h_mk_Sig x_512 =
317 let pi1 = x_512 in h_mk_Sig pi1 __
319 (** val sig_rect_Type3 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2 **)
320 let rec sig_rect_Type3 h_mk_Sig x_514 =
321 let pi1 = x_514 in h_mk_Sig pi1 __
323 (** val sig_rect_Type2 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2 **)
324 let rec sig_rect_Type2 h_mk_Sig x_516 =
325 let pi1 = x_516 in h_mk_Sig pi1 __
327 (** val sig_rect_Type1 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2 **)
328 let rec sig_rect_Type1 h_mk_Sig x_518 =
329 let pi1 = x_518 in h_mk_Sig pi1 __
331 (** val sig_rect_Type0 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2 **)
332 let rec sig_rect_Type0 h_mk_Sig x_520 =
333 let pi1 = x_520 in h_mk_Sig pi1 __
335 (** val pi1 : 'a1 sig0 -> 'a1 **)
339 (** val sig_inv_rect_Type4 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2 **)
340 let sig_inv_rect_Type4 hterm h1 =
341 let hcut = sig_rect_Type4 h1 hterm in hcut __
343 (** val sig_inv_rect_Type3 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2 **)
344 let sig_inv_rect_Type3 hterm h1 =
345 let hcut = sig_rect_Type3 h1 hterm in hcut __
347 (** val sig_inv_rect_Type2 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2 **)
348 let sig_inv_rect_Type2 hterm h1 =
349 let hcut = sig_rect_Type2 h1 hterm in hcut __
351 (** val sig_inv_rect_Type1 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2 **)
352 let sig_inv_rect_Type1 hterm h1 =
353 let hcut = sig_rect_Type1 h1 hterm in hcut __
355 (** val sig_inv_rect_Type0 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2 **)
356 let sig_inv_rect_Type0 hterm h1 =
357 let hcut = sig_rect_Type0 h1 hterm in hcut __
359 (** val sig_discr : 'a1 sig0 -> 'a1 sig0 -> __ **)
361 Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y
363 type ('a, 'b) prod = { fst : 'a; snd : 'b }
365 (** val prod_rect_Type4 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3 **)
366 let rec prod_rect_Type4 h_mk_Prod x_536 =
367 let { fst = fst0; snd = snd0 } = x_536 in h_mk_Prod fst0 snd0
369 (** val prod_rect_Type5 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3 **)
370 let rec prod_rect_Type5 h_mk_Prod x_538 =
371 let { fst = fst0; snd = snd0 } = x_538 in h_mk_Prod fst0 snd0
373 (** val prod_rect_Type3 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3 **)
374 let rec prod_rect_Type3 h_mk_Prod x_540 =
375 let { fst = fst0; snd = snd0 } = x_540 in h_mk_Prod fst0 snd0
377 (** val prod_rect_Type2 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3 **)
378 let rec prod_rect_Type2 h_mk_Prod x_542 =
379 let { fst = fst0; snd = snd0 } = x_542 in h_mk_Prod fst0 snd0
381 (** val prod_rect_Type1 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3 **)
382 let rec prod_rect_Type1 h_mk_Prod x_544 =
383 let { fst = fst0; snd = snd0 } = x_544 in h_mk_Prod fst0 snd0
385 (** val prod_rect_Type0 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3 **)
386 let rec prod_rect_Type0 h_mk_Prod x_546 =
387 let { fst = fst0; snd = snd0 } = x_546 in h_mk_Prod fst0 snd0
389 (** val fst : ('a1, 'a2) prod -> 'a1 **)
393 (** val snd : ('a1, 'a2) prod -> 'a2 **)
397 (** val prod_inv_rect_Type4 :
398 ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
399 let prod_inv_rect_Type4 hterm h1 =
400 let hcut = prod_rect_Type4 h1 hterm in hcut __
402 (** val prod_inv_rect_Type3 :
403 ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
404 let prod_inv_rect_Type3 hterm h1 =
405 let hcut = prod_rect_Type3 h1 hterm in hcut __
407 (** val prod_inv_rect_Type2 :
408 ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
409 let prod_inv_rect_Type2 hterm h1 =
410 let hcut = prod_rect_Type2 h1 hterm in hcut __
412 (** val prod_inv_rect_Type1 :
413 ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
414 let prod_inv_rect_Type1 hterm h1 =
415 let hcut = prod_rect_Type1 h1 hterm in hcut __
417 (** val prod_inv_rect_Type0 :
418 ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
419 let prod_inv_rect_Type0 hterm h1 =
420 let hcut = prod_rect_Type0 h1 hterm in hcut __
422 (** val prod_discr : ('a1, 'a2) prod -> ('a1, 'a2) prod -> __ **)
424 Logic.eq_rect_Type2 x
425 (let { fst = a0; snd = a10 } = x in Obj.magic (fun _ dH -> dH __ __)) y
427 (** val coerc_pair_sigma : ('a1, 'a2) prod -> ('a1, 'a2 sig0) prod **)
428 let coerc_pair_sigma clearme =
429 (let { fst = a; snd = b } = clearme in (fun _ -> { fst = a; snd = b })) __
431 (** val dpi1__o__coerc_pair_sigma :
432 (('a1, 'a2) prod, 'a3) dPair -> ('a1, 'a2 sig0) prod **)
433 let dpi1__o__coerc_pair_sigma x4 =
434 coerc_pair_sigma x4.dpi1