Ignore:
Timestamp:
Mar 7, 2011, 7:00:08 PM (10 years ago)
Author:
campbell
Message:

Oops, wrong bitvector negation.

File:
1 edited

Legend:

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

    r638 r648  
    134134definition ltu : int → int → bool ≝ lt_u wordsize.
    135135
    136 definition neg : int → int ≝ negation_bv wordsize.
     136definition neg : int → int ≝ two_complement_negation wordsize.
    137137
    138138let rec zero_ext (n:Z) (x:int) on x : int ≝
Note: See TracChangeset for help on using the changeset viewer.