Changeset 14 for C-semantics/Values.ma


Ignore:
Timestamp:
Jul 21, 2010, 3:08:58 PM (10 years ago)
Author:
campbell
Message:

Make Integers.ma respect bounds again, and reenable the rest of Mem.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Values.ma

    r3 r14  
    10071007  ∀chunk,v1,v2.
    10081008  Val_lessdef v1 v2 → Val_lessdef (load_result chunk v1) (load_result chunk v2).
    1009 #chunk;#v1;#v2;#H; ninversion H; //; ncases chunk; nnormalize; //;
     1009#chunk;#v1;#v2;#H; ninversion H; //; #v e1 e2; ncases chunk; nwhd in ⊢ (?%?); //;
    10101010nqed.
    10111011
Note: See TracChangeset for help on using the changeset viewer.