Ignore:
Timestamp:
Mar 4, 2011, 6:20:28 PM (9 years ago)
Author:
campbell
Message:

Switch to more conservative definitions in preparation for review.
(Efficient mul/div via Z, sort out some disambiguation problems that have
appeared.)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Integers.ma

    r582 r638  
    145145definition add ≝ addition_n wordsize.
    146146definition sub ≝ subtraction wordsize.
    147 definition mul ≝ λx,y. \fst (split ? wordsize wordsize (multiplication wordsize x y)).
     147(*definition mul ≝ λx,y. \fst (split ? wordsize wordsize (multiplication wordsize x y)).*)
     148definition mul ≝ λx,y. repr ((unsigned x) * (unsigned y)).
    148149definition Zdiv_round : Z → Z → Z ≝ λx,y: Z.
    149150  if Zltb x 0 then
Note: See TracChangeset for help on using the changeset viewer.