Ignore:
Timestamp:
Dec 13, 2011, 1:34:37 AM (8 years ago)
Author:
sacerdot
Message:

Start of merging of stuff into the standard library of Matita.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/binary/division.ma

    r1528 r1599  
    5050  ]
    5151| p0 m' ⇒
    52   match divide m' n with
    53   [ pair q r ⇒
     52  let 〈q,r〉 ≝ divide m' n in
    5453    match r with
    5554    [ pzero ⇒ 〈natp0 q,pzero〉
     
    6160      ]
    6261    ]
    63   ]
    6462| p1 m' ⇒
    65   match divide m' n with
    66   [ pair q r ⇒
     63  let 〈q,r〉 ≝ divide m' n in
    6764    match r with
    6865    [ pzero ⇒ match n with [ one ⇒ 〈natp1 q,pzero〉 | _ ⇒ 〈natp0 q,ppos one〉 ]
     
    7471      ]
    7572    ]
    76   ]
    7773].
    7874
     
    326322    [ OZ ⇒ OZ
    327323    | 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) ]
    330326    ]
    331327  | neg n ⇒
    332328    match y with
    333329    [ 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) ]
    336332    | neg m ⇒ natp_to_Z (fst ?? (divide n m))
    337333    ]
     
    345341    [ OZ ⇒ OZ
    346342    | 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) ]
    349345    ]
    350346  | neg n ⇒
    351347    match y with
    352348    [ 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) ]
    355351    | neg m ⇒ natp_to_Z (snd ?? (divide n m))
    356352    ]
Note: See TracChangeset for help on using the changeset viewer.