Changeset 2185 for src/joint/BEMem.ma


Ignore:
Timestamp:
Jul 13, 2012, 7:59:43 PM (8 years ago)
Author:
campbell
Message:

Use bitvectors for offsets.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/BEMem.ma

    r2176 r2185  
    118118*)
    119119lemma pointer_of_address_is_safe : ∀a : safe_address.pointer_of_address a = OK … (pointer_of_address_safe a).
    120 ** #a0 #a1 ***** #z #o 
     120** #a0 #a1 ***** #z #o
    121121#Hr
    122122(*
     
    127127destruct normalize
    128128@eqZb_elim [2,4,6: * #ABS elim (ABS (refl …))]
    129 @eqZb_elim [2,4,6: * #ABS elim (ABS (refl …))]
     129change with (eq_bv ???) in match (eq_v ?????);
     130@eq_bv_elim [2,4,6: * #ABS elim (ABS (refl …))]
    130131#_ #_ normalize %
    131132qed.
Note: See TracChangeset for help on using the changeset viewer.