Changeset 638 for Deliverables/D3.1/Csemantics/Integers.ma
 Timestamp:
 Mar 4, 2011, 6:20:28 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/Integers.ma
r582 r638 145 145 definition add ≝ addition_n wordsize. 146 146 definition 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)).*) 148 definition mul ≝ λx,y. repr ((unsigned x) * (unsigned y)). 148 149 definition Zdiv_round : Z → Z → Z ≝ λx,y: Z. 149 150 if Zltb x 0 then
Note: See TracChangeset
for help on using the changeset viewer.