Changeset 1215 for src/common


Ignore:
Timestamp:
Sep 15, 2011, 3:04:22 PM (8 years ago)
Author:
sacerdot
Message:

1) Added shifting directly on pointers
2) More temporary axioms closed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Pointers.ma

    r1213 r1215  
    9797 }.
    9898
     99definition shift_pointer: ∀n. pointer → BitVector n → pointer ≝
     100 λn,p,i. mk_pointer (ptype p) (pblock p) (pok p) (shift_offset n (poff p) i).
     101
     102definition neg_shift_pointer: ∀n. pointer → BitVector n → pointer ≝
     103 λn,p,i. mk_pointer (ptype p) (pblock p) (pok p) (neg_shift_offset n (poff p) i).
     104
    99105definition eq_pointer: pointer → pointer → bool ≝
    100106 λp1,p2.
Note: See TracChangeset for help on using the changeset viewer.