22 (** val compare_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1 **)
23 let rec compare_rect_Type4 h_LT h_EQ h_GT = function
28 (** val compare_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1 **)
29 let rec compare_rect_Type5 h_LT h_EQ h_GT = function
34 (** val compare_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1 **)
35 let rec compare_rect_Type3 h_LT h_EQ h_GT = function
40 (** val compare_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1 **)
41 let rec compare_rect_Type2 h_LT h_EQ h_GT = function
46 (** val compare_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1 **)
47 let rec compare_rect_Type1 h_LT h_EQ h_GT = function
52 (** val compare_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1 **)
53 let rec compare_rect_Type0 h_LT h_EQ h_GT = function
58 (** val compare_inv_rect_Type4 :
59 compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
60 let compare_inv_rect_Type4 hterm h1 h2 h3 =
61 let hcut = compare_rect_Type4 h1 h2 h3 hterm in hcut __
63 (** val compare_inv_rect_Type3 :
64 compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
65 let compare_inv_rect_Type3 hterm h1 h2 h3 =
66 let hcut = compare_rect_Type3 h1 h2 h3 hterm in hcut __
68 (** val compare_inv_rect_Type2 :
69 compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
70 let compare_inv_rect_Type2 hterm h1 h2 h3 =
71 let hcut = compare_rect_Type2 h1 h2 h3 hterm in hcut __
73 (** val compare_inv_rect_Type1 :
74 compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
75 let compare_inv_rect_Type1 hterm h1 h2 h3 =
76 let hcut = compare_rect_Type1 h1 h2 h3 hterm in hcut __
78 (** val compare_inv_rect_Type0 :
79 compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
80 let compare_inv_rect_Type0 hterm h1 h2 h3 =
81 let hcut = compare_rect_Type0 h1 h2 h3 hterm in hcut __
83 (** val compare_discr : compare -> compare -> __ **)
84 let compare_discr x y =
87 | LT -> Obj.magic (fun _ dH -> dH)
88 | EQ -> Obj.magic (fun _ dH -> dH)
89 | GT -> Obj.magic (fun _ dH -> dH)) y
91 (** val compare_invert : compare -> compare **)
92 let compare_invert = function
102 (** val pos_rect_Type4 :
103 'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1 **)
104 let rec pos_rect_Type4 h_one h_p1 h_p0 = function
106 | P1 x_1606 -> h_p1 x_1606 (pos_rect_Type4 h_one h_p1 h_p0 x_1606)
107 | P0 x_1607 -> h_p0 x_1607 (pos_rect_Type4 h_one h_p1 h_p0 x_1607)
109 (** val pos_rect_Type3 :
110 'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1 **)
111 let rec pos_rect_Type3 h_one h_p1 h_p0 = function
113 | P1 x_1618 -> h_p1 x_1618 (pos_rect_Type3 h_one h_p1 h_p0 x_1618)
114 | P0 x_1619 -> h_p0 x_1619 (pos_rect_Type3 h_one h_p1 h_p0 x_1619)
116 (** val pos_rect_Type2 :
117 'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1 **)
118 let rec pos_rect_Type2 h_one h_p1 h_p0 = function
120 | P1 x_1624 -> h_p1 x_1624 (pos_rect_Type2 h_one h_p1 h_p0 x_1624)
121 | P0 x_1625 -> h_p0 x_1625 (pos_rect_Type2 h_one h_p1 h_p0 x_1625)
123 (** val pos_rect_Type1 :
124 'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1 **)
125 let rec pos_rect_Type1 h_one h_p1 h_p0 = function
127 | P1 x_1630 -> h_p1 x_1630 (pos_rect_Type1 h_one h_p1 h_p0 x_1630)
128 | P0 x_1631 -> h_p0 x_1631 (pos_rect_Type1 h_one h_p1 h_p0 x_1631)
130 (** val pos_rect_Type0 :
131 'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1 **)
132 let rec pos_rect_Type0 h_one h_p1 h_p0 = function
134 | P1 x_1636 -> h_p1 x_1636 (pos_rect_Type0 h_one h_p1 h_p0 x_1636)
135 | P0 x_1637 -> h_p0 x_1637 (pos_rect_Type0 h_one h_p1 h_p0 x_1637)
137 (** val pos_inv_rect_Type4 :
138 pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
139 'a1) -> __ -> 'a1) -> 'a1 **)
140 let pos_inv_rect_Type4 hterm h1 h2 h3 =
141 let hcut = pos_rect_Type4 h1 h2 h3 hterm in hcut __
143 (** val pos_inv_rect_Type3 :
144 pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
145 'a1) -> __ -> 'a1) -> 'a1 **)
146 let pos_inv_rect_Type3 hterm h1 h2 h3 =
147 let hcut = pos_rect_Type3 h1 h2 h3 hterm in hcut __
149 (** val pos_inv_rect_Type2 :
150 pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
151 'a1) -> __ -> 'a1) -> 'a1 **)
152 let pos_inv_rect_Type2 hterm h1 h2 h3 =
153 let hcut = pos_rect_Type2 h1 h2 h3 hterm in hcut __
155 (** val pos_inv_rect_Type1 :
156 pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
157 'a1) -> __ -> 'a1) -> 'a1 **)
158 let pos_inv_rect_Type1 hterm h1 h2 h3 =
159 let hcut = pos_rect_Type1 h1 h2 h3 hterm in hcut __
161 (** val pos_inv_rect_Type0 :
162 pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
163 'a1) -> __ -> 'a1) -> 'a1 **)
164 let pos_inv_rect_Type0 hterm h1 h2 h3 =
165 let hcut = pos_rect_Type0 h1 h2 h3 hterm in hcut __
167 (** val pos_discr : pos -> pos -> __ **)
169 Logic.eq_rect_Type2 x
171 | One -> Obj.magic (fun _ dH -> dH)
172 | P1 a0 -> Obj.magic (fun _ dH -> dH __)
173 | P0 a0 -> Obj.magic (fun _ dH -> dH __)) y
175 (** val pred : pos -> pos **)
176 let rec pred = function
182 | P1 x -> P1 (pred ps)
183 | P0 x -> P1 (pred ps))
185 (** val succ : pos -> pos **)
186 let rec succ = function
188 | P1 ps -> P0 (succ ps)
191 (** val nat_of_pos : pos -> Nat.nat **)
192 let rec nat_of_pos = function
194 | P1 ps -> Nat.S (Nat.times (Nat.S (Nat.S Nat.O)) (nat_of_pos ps))
195 | P0 ps -> Nat.times (Nat.S (Nat.S Nat.O)) (nat_of_pos ps)
197 (** val succ_pos_of_nat : Nat.nat -> pos **)
198 let rec succ_pos_of_nat = function
200 | Nat.S n' -> succ (succ_pos_of_nat n')
202 (** val plus : pos -> pos -> pos **)
209 | P1 m' -> P0 (succ (plus n' m'))
210 | P0 m' -> P1 (plus n' m'))
214 | P1 m' -> P1 (plus n' m')
215 | P0 m' -> P0 (plus n' m'))
217 (** val times : pos -> pos -> pos **)
221 | P1 n' -> plus m (P0 (times n' m))
222 | P0 n' -> P0 (times n' m)
229 (** val minusresult_rect_Type4 :
230 'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1 **)
231 let rec minusresult_rect_Type4 h_MinusNeg h_MinusZero h_MinusPos = function
232 | MinusNeg -> h_MinusNeg
233 | MinusZero -> h_MinusZero
234 | MinusPos x_1813 -> h_MinusPos x_1813
236 (** val minusresult_rect_Type5 :
237 'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1 **)
238 let rec minusresult_rect_Type5 h_MinusNeg h_MinusZero h_MinusPos = function
239 | MinusNeg -> h_MinusNeg
240 | MinusZero -> h_MinusZero
241 | MinusPos x_1818 -> h_MinusPos x_1818
243 (** val minusresult_rect_Type3 :
244 'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1 **)
245 let rec minusresult_rect_Type3 h_MinusNeg h_MinusZero h_MinusPos = function
246 | MinusNeg -> h_MinusNeg
247 | MinusZero -> h_MinusZero
248 | MinusPos x_1823 -> h_MinusPos x_1823
250 (** val minusresult_rect_Type2 :
251 'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1 **)
252 let rec minusresult_rect_Type2 h_MinusNeg h_MinusZero h_MinusPos = function
253 | MinusNeg -> h_MinusNeg
254 | MinusZero -> h_MinusZero
255 | MinusPos x_1828 -> h_MinusPos x_1828
257 (** val minusresult_rect_Type1 :
258 'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1 **)
259 let rec minusresult_rect_Type1 h_MinusNeg h_MinusZero h_MinusPos = function
260 | MinusNeg -> h_MinusNeg
261 | MinusZero -> h_MinusZero
262 | MinusPos x_1833 -> h_MinusPos x_1833
264 (** val minusresult_rect_Type0 :
265 'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1 **)
266 let rec minusresult_rect_Type0 h_MinusNeg h_MinusZero h_MinusPos = function
267 | MinusNeg -> h_MinusNeg
268 | MinusZero -> h_MinusZero
269 | MinusPos x_1838 -> h_MinusPos x_1838
271 (** val minusresult_inv_rect_Type4 :
272 minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1 **)
273 let minusresult_inv_rect_Type4 hterm h1 h2 h3 =
274 let hcut = minusresult_rect_Type4 h1 h2 h3 hterm in hcut __
276 (** val minusresult_inv_rect_Type3 :
277 minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1 **)
278 let minusresult_inv_rect_Type3 hterm h1 h2 h3 =
279 let hcut = minusresult_rect_Type3 h1 h2 h3 hterm in hcut __
281 (** val minusresult_inv_rect_Type2 :
282 minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1 **)
283 let minusresult_inv_rect_Type2 hterm h1 h2 h3 =
284 let hcut = minusresult_rect_Type2 h1 h2 h3 hterm in hcut __
286 (** val minusresult_inv_rect_Type1 :
287 minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1 **)
288 let minusresult_inv_rect_Type1 hterm h1 h2 h3 =
289 let hcut = minusresult_rect_Type1 h1 h2 h3 hterm in hcut __
291 (** val minusresult_inv_rect_Type0 :
292 minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1 **)
293 let minusresult_inv_rect_Type0 hterm h1 h2 h3 =
294 let hcut = minusresult_rect_Type0 h1 h2 h3 hterm in hcut __
296 (** val minusresult_discr : minusresult -> minusresult -> __ **)
297 let minusresult_discr x y =
298 Logic.eq_rect_Type2 x
300 | MinusNeg -> Obj.magic (fun _ dH -> dH)
301 | MinusZero -> Obj.magic (fun _ dH -> dH)
302 | MinusPos a0 -> Obj.magic (fun _ dH -> dH __)) y
304 (** val partial_minus : pos -> pos -> minusresult **)
305 let rec partial_minus n m =
314 | One -> MinusPos (P0 n')
316 (match partial_minus n' m' with
317 | MinusNeg -> MinusNeg
318 | MinusZero -> MinusZero
319 | MinusPos p -> MinusPos (P0 p))
321 (match partial_minus n' m' with
322 | MinusNeg -> MinusNeg
323 | MinusZero -> MinusPos One
324 | MinusPos p -> MinusPos (P1 p)))
327 | One -> MinusPos (pred n)
329 (match partial_minus n' m' with
330 | MinusNeg -> MinusNeg
331 | MinusZero -> MinusNeg
332 | MinusPos p -> MinusPos (pred (P0 p)))
334 (match partial_minus n' m' with
335 | MinusNeg -> MinusNeg
336 | MinusZero -> MinusZero
337 | MinusPos p -> MinusPos (P0 p)))
339 (** val minus : pos -> pos -> pos **)
341 match partial_minus n m with
346 (** val eqb : pos -> pos -> Bool.bool **)
353 | P0 x -> Bool.False)
358 | P0 x -> Bool.False)
365 (** val eqb_elim : pos -> pos -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
366 let eqb_elim n m x x0 =
367 pos_rect_Type1 (fun m0 ->
369 | One -> (fun _ auto auto' -> auto __)
370 | P1 m' -> (fun _ t f -> f __)
371 | P0 m' -> (fun _ t f -> f __)) (fun n' iH m0 ->
373 | One -> (fun _ t f -> f __)
374 | P1 m' -> (fun _ t f -> iH m' __ (fun _ -> t __) (fun _ -> f __))
375 | P0 m' -> (fun _ t f -> f __)) (fun n' iH m0 ->
377 | One -> (fun _ t f -> f __)
378 | P1 m' -> (fun _ t f -> f __)
379 | P0 m' -> (fun _ t f -> iH m' __ (fun _ -> t __) (fun _ -> f __))) n m
382 (** val leb : pos -> pos -> Bool.bool **)
384 match partial_minus n m with
385 | MinusNeg -> Bool.True
386 | MinusZero -> Bool.True
387 | MinusPos x -> Bool.False
389 (** val pos_compare : pos -> pos -> compare **)
390 let pos_compare n m =
391 match partial_minus n m with
396 (** val two_power_nat : Nat.nat -> pos **)
397 let rec two_power_nat = function
399 | Nat.S n' -> P0 (two_power_nat n')
401 (** val two_power_pos : pos -> pos **)
402 let two_power_pos p =
403 two_power_nat (nat_of_pos p)
405 (** val max : pos -> pos -> pos **)