11 open Hints_declaration
25 | Ppos of Positive.pos
27 (** val natp_rect_Type4 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 **)
28 let rec natp_rect_Type4 h_pzero h_ppos = function
30 | Ppos x_4901 -> h_ppos x_4901
32 (** val natp_rect_Type5 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 **)
33 let rec natp_rect_Type5 h_pzero h_ppos = function
35 | Ppos x_4905 -> h_ppos x_4905
37 (** val natp_rect_Type3 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 **)
38 let rec natp_rect_Type3 h_pzero h_ppos = function
40 | Ppos x_4909 -> h_ppos x_4909
42 (** val natp_rect_Type2 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 **)
43 let rec natp_rect_Type2 h_pzero h_ppos = function
45 | Ppos x_4913 -> h_ppos x_4913
47 (** val natp_rect_Type1 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 **)
48 let rec natp_rect_Type1 h_pzero h_ppos = function
50 | Ppos x_4917 -> h_ppos x_4917
52 (** val natp_rect_Type0 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 **)
53 let rec natp_rect_Type0 h_pzero h_ppos = function
55 | Ppos x_4921 -> h_ppos x_4921
57 (** val natp_inv_rect_Type4 :
58 natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
59 let natp_inv_rect_Type4 hterm h1 h2 =
60 let hcut = natp_rect_Type4 h1 h2 hterm in hcut __
62 (** val natp_inv_rect_Type3 :
63 natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
64 let natp_inv_rect_Type3 hterm h1 h2 =
65 let hcut = natp_rect_Type3 h1 h2 hterm in hcut __
67 (** val natp_inv_rect_Type2 :
68 natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
69 let natp_inv_rect_Type2 hterm h1 h2 =
70 let hcut = natp_rect_Type2 h1 h2 hterm in hcut __
72 (** val natp_inv_rect_Type1 :
73 natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
74 let natp_inv_rect_Type1 hterm h1 h2 =
75 let hcut = natp_rect_Type1 h1 h2 hterm in hcut __
77 (** val natp_inv_rect_Type0 :
78 natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
79 let natp_inv_rect_Type0 hterm h1 h2 =
80 let hcut = natp_rect_Type0 h1 h2 hterm in hcut __
82 (** val natp_discr : natp -> natp -> __ **)
86 | Pzero -> Obj.magic (fun _ dH -> dH)
87 | Ppos a0 -> Obj.magic (fun _ dH -> dH __)) y
89 (** val natp0 : natp -> natp **)
92 | Ppos m -> Ppos (Positive.P0 m)
94 (** val natp1 : natp -> natp **)
96 | Pzero -> Ppos Positive.One
97 | Ppos m -> Ppos (Positive.P1 m)
99 (** val divide : Positive.pos -> Positive.pos -> (natp, natp) Types.prod **)
104 | Positive.One -> { Types.fst = (Ppos Positive.One); Types.snd = Pzero }
106 { Types.fst = Pzero; Types.snd = (Ppos Positive.One) }
108 { Types.fst = Pzero; Types.snd = (Ppos Positive.One) })
110 let { Types.fst = q; Types.snd = r } = divide m' n in
114 | Positive.One -> { Types.fst = (natp1 q); Types.snd = Pzero }
116 { Types.fst = (natp0 q); Types.snd = (Ppos Positive.One) }
118 { Types.fst = (natp0 q); Types.snd = (Ppos Positive.One) })
120 (match Positive.partial_minus (Positive.P1 r') n with
121 | Positive.MinusNeg ->
122 { Types.fst = (natp0 q); Types.snd = (Ppos (Positive.P1 r')) }
123 | Positive.MinusZero -> { Types.fst = (natp1 q); Types.snd = Pzero }
124 | Positive.MinusPos r'' ->
125 { Types.fst = (natp1 q); Types.snd = (Ppos r'') }))
127 let { Types.fst = q; Types.snd = r } = divide m' n in
129 | Pzero -> { Types.fst = (natp0 q); Types.snd = Pzero }
131 (match Positive.partial_minus (Positive.P0 r') n with
132 | Positive.MinusNeg ->
133 { Types.fst = (natp0 q); Types.snd = (Ppos (Positive.P0 r')) }
134 | Positive.MinusZero -> { Types.fst = (natp1 q); Types.snd = Pzero }
135 | Positive.MinusPos r'' ->
136 { Types.fst = (natp1 q); Types.snd = (Ppos r'') }))
138 (** val div : Positive.pos -> Positive.pos -> natp **)
140 (divide m n).Types.fst
142 (** val mod0 : Positive.pos -> Positive.pos -> natp **)
144 (divide m n).Types.snd
146 (** val natp_plus : natp -> natp -> natp **)
147 let rec natp_plus n m =
153 | Ppos m' -> Ppos (Positive.plus n' m'))
155 (** val natp_times : natp -> natp -> natp **)
156 let rec natp_times n m =
162 | Ppos m' -> Ppos (Positive.times n' m'))
164 (** val dec_divides : Positive.pos -> Positive.pos -> (__, __) Types.sum **)
165 let dec_divides m n =
166 Types.prod_rect_Type0 (fun dv md ->
170 | Pzero -> (fun _ -> Obj.magic natp_discr (Ppos n) Pzero __ __)
171 | Ppos dv' -> (fun _ -> Types.Inl __))
174 | Pzero -> (fun md' _ -> Types.Inr __)
175 | Ppos md' -> (fun dv' _ -> Types.Inr __)) x) (divide n m) __
177 (** val dec_dividesZ : Z.z -> Z.z -> (__, __) Types.sum **)
178 let dec_dividesZ p q =
182 | Z.OZ -> Types.Inr __
183 | Z.Pos m -> Types.Inr __
184 | Z.Neg m -> Types.Inr __)
187 | Z.OZ -> Types.Inl __
188 | Z.Pos auto -> dec_divides n auto
189 | Z.Neg auto -> dec_divides n auto)
192 | Z.OZ -> Types.Inl __
193 | Z.Pos auto -> dec_divides n auto
194 | Z.Neg auto -> dec_divides n auto)
196 (** val natp_to_Z : natp -> Z.z **)
197 let natp_to_Z = function
201 (** val natp_to_negZ : natp -> Z.z **)
202 let natp_to_negZ = function
206 (** val divZ : Z.z -> Z.z -> Z.z **)
213 | Z.Pos m -> natp_to_Z (divide n m).Types.fst
215 let { Types.fst = q; Types.snd = r } = divide n m in
217 | Pzero -> natp_to_negZ q
218 | Ppos x0 -> Z.zpred (natp_to_negZ q)))
223 let { Types.fst = q; Types.snd = r } = divide n m in
225 | Pzero -> natp_to_negZ q
226 | Ppos x0 -> Z.zpred (natp_to_negZ q))
227 | Z.Neg m -> natp_to_Z (divide n m).Types.fst)
229 (** val modZ : Z.z -> Z.z -> Z.z **)
236 | Z.Pos m -> natp_to_Z (divide n m).Types.snd
238 let { Types.fst = q; Types.snd = r } = divide n m in
241 | Ppos x0 -> Z.zplus y (natp_to_Z r)))
246 let { Types.fst = q; Types.snd = r } = divide n m in
249 | Ppos x0 -> Z.zminus y (natp_to_Z r))
250 | Z.Neg m -> natp_to_Z (divide n m).Types.snd)