Changeset 1599 for src/utilities/binary/division.ma
 Timestamp:
 Dec 13, 2011, 1:34:37 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/binary/division.ma
r1528 r1599 50 50 ] 51 51  p0 m' ⇒ 52 match divide m' n with 53 [ pair q r ⇒ 52 let 〈q,r〉 ≝ divide m' n in 54 53 match r with 55 54 [ pzero ⇒ 〈natp0 q,pzero〉 … … 61 60 ] 62 61 ] 63 ]64 62  p1 m' ⇒ 65 match divide m' n with 66 [ pair q r ⇒ 63 let 〈q,r〉 ≝ divide m' n in 67 64 match r with 68 65 [ pzero ⇒ match n with [ one ⇒ 〈natp1 q,pzero〉  _ ⇒ 〈natp0 q,ppos one〉 ] … … 74 71 ] 75 72 ] 76 ]77 73 ]. 78 74 … … 326 322 [ OZ ⇒ OZ 327 323  pos m ⇒ natp_to_Z (fst ?? (divide n m)) 328  neg m ⇒ match divide n m with [ pair q r ⇒329 match r with [ pzero ⇒ natp_to_negZ q  _ ⇒ Zpred (natp_to_negZ q) ] ]324  neg m ⇒ let 〈q,r〉 ≝ divide n m in 325 match r with [ pzero ⇒ natp_to_negZ q  _ ⇒ Zpred (natp_to_negZ q) ] 330 326 ] 331 327  neg n ⇒ 332 328 match y with 333 329 [ OZ ⇒ OZ 334  pos m ⇒ match divide n m with [ pair q r ⇒335 match r with [ pzero ⇒ natp_to_negZ q  _ ⇒ Zpred (natp_to_negZ q) ] ]330  pos m ⇒ let 〈q,r〉 ≝ divide n m in 331 match r with [ pzero ⇒ natp_to_negZ q  _ ⇒ Zpred (natp_to_negZ q) ] 336 332  neg m ⇒ natp_to_Z (fst ?? (divide n m)) 337 333 ] … … 345 341 [ OZ ⇒ OZ 346 342  pos m ⇒ natp_to_Z (snd ?? (divide n m)) 347  neg m ⇒ match divide n m with [ pair q r ⇒348 match r with [ pzero ⇒ OZ  _ ⇒ y+(natp_to_Z r) ] ]343  neg m ⇒ let 〈q,r〉 ≝ divide n m in 344 match r with [ pzero ⇒ OZ  _ ⇒ y+(natp_to_Z r) ] 349 345 ] 350 346  neg n ⇒ 351 347 match y with 352 348 [ OZ ⇒ OZ 353  pos m ⇒ match divide n m with [ pair q r ⇒354 match r with [ pzero ⇒ OZ  _ ⇒ y(natp_to_Z r) ] ]349  pos m ⇒ let 〈q,r〉 ≝ divide n m in 350 match r with [ pzero ⇒ OZ  _ ⇒ y(natp_to_Z r) ] 355 351  neg m ⇒ natp_to_Z (snd ?? (divide n m)) 356 352 ]
Note: See TracChangeset
for help on using the changeset viewer.