Changeset 2177 for src/ASM


Ignore:
Timestamp:
Jul 12, 2012, 2:56:50 PM (7 years ago)
Author:
campbell
Message:

Tidy up multiplication.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r2154 r2177  
    364364  ].
    365365
     366definition short_multiplication : ∀n:nat. BitVector n → BitVector n → BitVector n ≝
     367λn,x,y. (\snd (vsplit ??? (multiplication ? x y))).
     368
    366369(* Division:  001...000 divided by 000...010
    367370     Shift the divisor as far left as possible,
Note: See TracChangeset for help on using the changeset viewer.