Changeset 1599 for src/utilities/binary
- Timestamp:
- Dec 13, 2011, 1:34:37 AM (9 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.