24 (** val z_rect_Type4 :
25 'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 **)
26 let rec z_rect_Type4 h_OZ h_pos h_neg = function
28 | Pos x_4786 -> h_pos x_4786
29 | Neg x_4787 -> h_neg x_4787
31 (** val z_rect_Type5 :
32 'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 **)
33 let rec z_rect_Type5 h_OZ h_pos h_neg = function
35 | Pos x_4792 -> h_pos x_4792
36 | Neg x_4793 -> h_neg x_4793
38 (** val z_rect_Type3 :
39 'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 **)
40 let rec z_rect_Type3 h_OZ h_pos h_neg = function
42 | Pos x_4798 -> h_pos x_4798
43 | Neg x_4799 -> h_neg x_4799
45 (** val z_rect_Type2 :
46 'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 **)
47 let rec z_rect_Type2 h_OZ h_pos h_neg = function
49 | Pos x_4804 -> h_pos x_4804
50 | Neg x_4805 -> h_neg x_4805
52 (** val z_rect_Type1 :
53 'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 **)
54 let rec z_rect_Type1 h_OZ h_pos h_neg = function
56 | Pos x_4810 -> h_pos x_4810
57 | Neg x_4811 -> h_neg x_4811
59 (** val z_rect_Type0 :
60 'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 **)
61 let rec z_rect_Type0 h_OZ h_pos h_neg = function
63 | Pos x_4816 -> h_pos x_4816
64 | Neg x_4817 -> h_neg x_4817
66 (** val z_inv_rect_Type4 :
67 z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
69 let z_inv_rect_Type4 hterm h1 h2 h3 =
70 let hcut = z_rect_Type4 h1 h2 h3 hterm in hcut __
72 (** val z_inv_rect_Type3 :
73 z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
75 let z_inv_rect_Type3 hterm h1 h2 h3 =
76 let hcut = z_rect_Type3 h1 h2 h3 hterm in hcut __
78 (** val z_inv_rect_Type2 :
79 z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
81 let z_inv_rect_Type2 hterm h1 h2 h3 =
82 let hcut = z_rect_Type2 h1 h2 h3 hterm in hcut __
84 (** val z_inv_rect_Type1 :
85 z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
87 let z_inv_rect_Type1 hterm h1 h2 h3 =
88 let hcut = z_rect_Type1 h1 h2 h3 hterm in hcut __
90 (** val z_inv_rect_Type0 :
91 z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
93 let z_inv_rect_Type0 hterm h1 h2 h3 =
94 let hcut = z_rect_Type0 h1 h2 h3 hterm in hcut __
96 (** val z_discr : z -> z -> __ **)
100 | OZ -> Obj.magic (fun _ dH -> dH)
101 | Pos a0 -> Obj.magic (fun _ dH -> dH __)
102 | Neg a0 -> Obj.magic (fun _ dH -> dH __)) y
104 (** val z_of_nat : Nat.nat -> z **)
105 let z_of_nat = function
107 | Nat.S n0 -> Pos (Positive.succ_pos_of_nat n0)
109 (** val neg_Z_of_nat : Nat.nat -> z **)
110 let neg_Z_of_nat = function
112 | Nat.S n0 -> Neg (Positive.succ_pos_of_nat n0)
114 (** val abs : z -> Nat.nat **)
117 | Pos n -> Positive.nat_of_pos n
118 | Neg n -> Positive.nat_of_pos n
120 (** val oZ_test : z -> Bool.bool **)
121 let oZ_test = function
123 | Pos x -> Bool.False
124 | Neg x -> Bool.False
126 (** val zsucc : z -> z **)
128 | OZ -> Pos Positive.One
129 | Pos n -> Pos (Positive.succ n)
133 | Positive.P1 x -> Neg (Positive.pred n)
134 | Positive.P0 x -> Neg (Positive.pred n))
136 (** val zpred : z -> z **)
138 | OZ -> Neg Positive.One
142 | Positive.P1 x -> Pos (Positive.pred n)
143 | Positive.P0 x -> Pos (Positive.pred n))
144 | Neg n -> Neg (Positive.succ n)
146 (** val eqZb : z -> z -> Bool.bool **)
152 | Pos q -> Bool.False
153 | Neg q -> Bool.False)
157 | Pos q -> Positive.eqb p q
158 | Neg q -> Bool.False)
162 | Pos q -> Bool.False
163 | Neg q -> Positive.eqb p q)
165 (** val z_compare : z -> z -> Positive.compare **)
166 let rec z_compare x y =
171 | Pos m -> Positive.LT
172 | Neg m -> Positive.GT)
176 | Pos m -> Positive.pos_compare n m
177 | Neg m -> Positive.GT)
181 | Pos m -> Positive.LT
182 | Neg m -> Positive.pos_compare m n)
184 (** val zplus : z -> z -> z **)
191 | Pos n -> Pos (Positive.plus m n)
193 (match Positive.pos_compare m n with
194 | Positive.LT -> Neg (Positive.minus n m)
196 | Positive.GT -> Pos (Positive.minus m n)))
201 (match Positive.pos_compare m n with
202 | Positive.LT -> Pos (Positive.minus n m)
204 | Positive.GT -> Neg (Positive.minus m n))
205 | Neg n -> Neg (Positive.plus m n))
207 (** val zopp : z -> z **)
213 (** val zminus : z -> z -> z **)
217 (** val z_two_power_nat : Nat.nat -> z **)
218 let z_two_power_nat n =
219 Pos (Positive.two_power_nat n)
221 (** val z_two_power_pos : Positive.pos -> z **)
222 let z_two_power_pos n =
223 Pos (Positive.two_power_pos n)
225 (** val two_p : z -> z **)
227 | OZ -> Pos Positive.One
228 | Pos p -> Pos (Positive.two_power_pos p)
233 (** val decidable_eq_Z_Type : z -> z -> (__, __) Types.sum **)
234 let decidable_eq_Z_Type z1 z2 =
235 (match eqZb z1 z2 with
236 | Bool.True -> (fun _ -> Types.Inl __)
237 | Bool.False -> (fun _ -> Types.Inr __)) __
239 (** val zleb : z -> z -> Bool.bool **)
246 | Neg m -> Bool.False)
250 | Pos m -> Positive.leb n m
251 | Neg m -> Bool.False)
256 | Neg m -> Positive.leb m n)
258 (** val zltb : z -> z -> Bool.bool **)
265 | Neg m -> Bool.False)
269 | Pos m -> Positive.leb (Positive.succ n) m
270 | Neg m -> Bool.False)
275 | Neg m -> Positive.leb (Positive.succ m) n)
277 (** val zleb_elim_Type0 : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
278 let zleb_elim_Type0 n m hle hnle =
279 Bool.bool_rect_Type0 (fun _ -> hle __) (fun _ -> hnle __) (zleb n m) __
281 (** val zltb_elim_Type0 : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
282 let zltb_elim_Type0 n m hlt hnlt =
283 Bool.bool_rect_Type0 (fun _ -> hlt __) (fun _ -> hnlt __) (zltb n m) __
285 (** val z_times : z -> z -> z **)
286 let rec z_times x y =
292 | Pos m -> Pos (Positive.times n m)
293 | Neg m -> Neg (Positive.times n m))
297 | Pos m -> Neg (Positive.times n m)
298 | Neg m -> Pos (Positive.times n m))
300 (** val zmax : z -> z -> z **)
302 match z_compare x y with