Changeset 2773 for extracted/positive.ml
 Timestamp:
 Mar 4, 2013, 10:03:33 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/positive.ml
r2601 r2773 104 104 let rec pos_rect_Type4 h_one h_p1 h_p0 = function 105 105  One > h_one 106  P1 x_1 375 > h_p1 x_1375 (pos_rect_Type4 h_one h_p1 h_p0 x_1375)107  P0 x_1 376 > h_p0 x_1376 (pos_rect_Type4 h_one h_p1 h_p0 x_1376)106  P1 x_1037 > h_p1 x_1037 (pos_rect_Type4 h_one h_p1 h_p0 x_1037) 107  P0 x_1038 > h_p0 x_1038 (pos_rect_Type4 h_one h_p1 h_p0 x_1038) 108 108 109 109 (** val pos_rect_Type3 : … … 111 111 let rec pos_rect_Type3 h_one h_p1 h_p0 = function 112 112  One > h_one 113  P1 x_1 387 > h_p1 x_1387 (pos_rect_Type3 h_one h_p1 h_p0 x_1387)114  P0 x_1 388 > h_p0 x_1388 (pos_rect_Type3 h_one h_p1 h_p0 x_1388)113  P1 x_1049 > h_p1 x_1049 (pos_rect_Type3 h_one h_p1 h_p0 x_1049) 114  P0 x_1050 > h_p0 x_1050 (pos_rect_Type3 h_one h_p1 h_p0 x_1050) 115 115 116 116 (** val pos_rect_Type2 : … … 118 118 let rec pos_rect_Type2 h_one h_p1 h_p0 = function 119 119  One > h_one 120  P1 x_1 393 > h_p1 x_1393 (pos_rect_Type2 h_one h_p1 h_p0 x_1393)121  P0 x_1 394 > h_p0 x_1394 (pos_rect_Type2 h_one h_p1 h_p0 x_1394)120  P1 x_1055 > h_p1 x_1055 (pos_rect_Type2 h_one h_p1 h_p0 x_1055) 121  P0 x_1056 > h_p0 x_1056 (pos_rect_Type2 h_one h_p1 h_p0 x_1056) 122 122 123 123 (** val pos_rect_Type1 : … … 125 125 let rec pos_rect_Type1 h_one h_p1 h_p0 = function 126 126  One > h_one 127  P1 x_1 399 > h_p1 x_1399 (pos_rect_Type1 h_one h_p1 h_p0 x_1399)128  P0 x_1 400 > h_p0 x_1400 (pos_rect_Type1 h_one h_p1 h_p0 x_1400)127  P1 x_1061 > h_p1 x_1061 (pos_rect_Type1 h_one h_p1 h_p0 x_1061) 128  P0 x_1062 > h_p0 x_1062 (pos_rect_Type1 h_one h_p1 h_p0 x_1062) 129 129 130 130 (** val pos_rect_Type0 : … … 132 132 let rec pos_rect_Type0 h_one h_p1 h_p0 = function 133 133  One > h_one 134  P1 x_1 405 > h_p1 x_1405 (pos_rect_Type0 h_one h_p1 h_p0 x_1405)135  P0 x_1 406 > h_p0 x_1406 (pos_rect_Type0 h_one h_p1 h_p0 x_1406)134  P1 x_1067 > h_p1 x_1067 (pos_rect_Type0 h_one h_p1 h_p0 x_1067) 135  P0 x_1068 > h_p0 x_1068 (pos_rect_Type0 h_one h_p1 h_p0 x_1068) 136 136 137 137 (** val pos_inv_rect_Type4 : … … 173 173  P0 a0 > Obj.magic (fun _ dH > dH __)) y 174 174 175 (** val pred 0: pos > pos **)176 let rec pred 0= function175 (** val pred : pos > pos **) 176 let rec pred = function 177 177  One > One 178 178  P1 ps > P0 ps … … 180 180 (match ps with 181 181  One > One 182  P1 x > P1 (pred 0ps)183  P0 x > P1 (pred 0ps))182  P1 x > P1 (pred ps) 183  P0 x > P1 (pred ps)) 184 184 185 185 (** val succ : pos > pos **) … … 200 200  Nat.S n' > succ (succ_pos_of_nat n') 201 201 202 (** val plus 0: pos > pos > pos **)203 let rec plus 0n m =202 (** val plus : pos > pos > pos **) 203 let rec plus n m = 204 204 match n with 205 205  One > succ m … … 207 207 (match m with 208 208  One > succ n 209  P1 m' > P0 (succ (plus 0n' m'))210  P0 m' > P1 (plus 0n' m'))209  P1 m' > P0 (succ (plus n' m')) 210  P0 m' > P1 (plus n' m')) 211 211  P0 n' > 212 212 (match m with 213 213  One > P1 n' 214  P1 m' > P1 (plus 0n' m')215  P0 m' > P0 (plus 0n' m'))216 217 (** val times 0: pos > pos > pos **)218 let rec times 0n m =214  P1 m' > P1 (plus n' m') 215  P0 m' > P0 (plus n' m')) 216 217 (** val times : pos > pos > pos **) 218 let rec times n m = 219 219 match n with 220 220  One > m 221  P1 n' > plus 0 m (P0 (times0n' m))222  P0 n' > P0 (times 0n' m)221  P1 n' > plus m (P0 (times n' m)) 222  P0 n' > P0 (times n' m) 223 223 224 224 type minusresult = … … 232 232  MinusNeg > h_MinusNeg 233 233  MinusZero > h_MinusZero 234  MinusPos x_1 582 > h_MinusPos x_1582234  MinusPos x_1244 > h_MinusPos x_1244 235 235 236 236 (** val minusresult_rect_Type5 : … … 239 239  MinusNeg > h_MinusNeg 240 240  MinusZero > h_MinusZero 241  MinusPos x_1 587 > h_MinusPos x_1587241  MinusPos x_1249 > h_MinusPos x_1249 242 242 243 243 (** val minusresult_rect_Type3 : … … 246 246  MinusNeg > h_MinusNeg 247 247  MinusZero > h_MinusZero 248  MinusPos x_1 592 > h_MinusPos x_1592248  MinusPos x_1254 > h_MinusPos x_1254 249 249 250 250 (** val minusresult_rect_Type2 : … … 253 253  MinusNeg > h_MinusNeg 254 254  MinusZero > h_MinusZero 255  MinusPos x_1 597 > h_MinusPos x_1597255  MinusPos x_1259 > h_MinusPos x_1259 256 256 257 257 (** val minusresult_rect_Type1 : … … 260 260  MinusNeg > h_MinusNeg 261 261  MinusZero > h_MinusZero 262  MinusPos x_1 602 > h_MinusPos x_1602262  MinusPos x_1264 > h_MinusPos x_1264 263 263 264 264 (** val minusresult_rect_Type0 : … … 267 267  MinusNeg > h_MinusNeg 268 268  MinusZero > h_MinusZero 269  MinusPos x_1 607 > h_MinusPos x_1607269  MinusPos x_1269 > h_MinusPos x_1269 270 270 271 271 (** val minusresult_inv_rect_Type4 : … … 325 325  P0 n' > 326 326 (match m with 327  One > MinusPos (pred 0n)327  One > MinusPos (pred n) 328 328  P1 m' > 329 329 (match partial_minus n' m' with 330 330  MinusNeg > MinusNeg 331 331  MinusZero > MinusNeg 332  MinusPos p > MinusPos (pred 0(P0 p)))332  MinusPos p > MinusPos (pred (P0 p))) 333 333  P0 m' > 334 334 (match partial_minus n' m' with … … 337 337  MinusPos p > MinusPos (P0 p))) 338 338 339 (** val minus 0: pos > pos > pos **)340 let minus 0n m =339 (** val minus : pos > pos > pos **) 340 let minus n m = 341 341 match partial_minus n m with 342 342  MinusNeg > One … … 344 344  MinusPos p > p 345 345 346 (** val eqb 0: pos > pos > Bool.bool **)347 let rec eqb 0n m =346 (** val eqb : pos > pos > Bool.bool **) 347 let rec eqb n m = 348 348 match n with 349 349  One > … … 355 355 (match m with 356 356  One > Bool.False 357  P1 q > eqb 0p q357  P1 q > eqb p q 358 358  P0 x > Bool.False) 359 359  P0 p > … … 361 361  One > Bool.False 362 362  P1 x > Bool.False 363  P0 q > eqb 0p q)363  P0 q > eqb p q) 364 364 365 365 (** val eqb_elim : pos > pos > (__ > 'a1) > (__ > 'a1) > 'a1 **) … … 380 380 __ x x0 381 381 382 (** val leb 0: pos > pos > Bool.bool **)383 let rec leb 0n m =382 (** val leb : pos > pos > Bool.bool **) 383 let rec leb n m = 384 384 match partial_minus n m with 385 385  MinusNeg > Bool.True … … 403 403 two_power_nat (nat_of_pos p) 404 404 405 (** val max 0: pos > pos > pos **)406 let max 0n m =407 match leb 0n m with405 (** val max : pos > pos > pos **) 406 let max n m = 407 match leb n m with 408 408  Bool.True > m 409 409  Bool.False > n
Note: See TracChangeset
for help on using the changeset viewer.