Changeset 1215 for src/common

Timestamp:

Sep 15, 2011, 3:04:22 PM (10 years ago)

Author:

sacerdot

Message:

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

File:

• src/common/Pointers.ma (modified) (1 diff)

src/common/Pointers.ma

@@ -97 +97 @@
  }.
 
+definition shift_pointer: ∀n. pointer → BitVector n → pointer ≝
+ λn,p,i. mk_pointer (ptype p) (pblock p) (pok p) (shift_offset n (poff p) i).
+
+definition neg_shift_pointer: ∀n. pointer → BitVector n → pointer ≝
+ λn,p,i. mk_pointer (ptype p) (pblock p) (pok p) (neg_shift_offset n (poff p) i).
+
 definition eq_pointer: pointer → pointer → bool ≝
  λp1,p2.