Ignore:
Timestamp:
Nov 23, 2011, 6:03:07 PM (8 years ago)
Author:
campbell
Message:

Use pointer record in front-end.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Pointers.ma

    r1516 r1545  
    100100 λn,p,i. mk_pointer (ptype p) (pblock p) (pok p) (shift_offset n (poff p) i).
    101101
     102(* multiply shift by a nat (i.e., sizeof) without danger of overflow *)
     103definition shift_pointer_n: ∀n. pointer → nat → BitVector n → pointer ≝
     104 λn,p,i,j. mk_pointer (ptype p) (pblock p) (pok p) (shift_offset_n n (poff p) i j).
     105
    102106definition neg_shift_pointer: ∀n. pointer → BitVector n → pointer ≝
    103107 λn,p,i. mk_pointer (ptype p) (pblock p) (pok p) (neg_shift_offset n (poff p) i).
     108
     109definition neg_shift_pointer_n: ∀n. pointer → nat → BitVector n → pointer ≝
     110 λn,p,i,j. mk_pointer (ptype p) (pblock p) (pok p) (neg_shift_offset_n n (poff p) i j).
    104111
    105112definition eq_pointer: pointer → pointer → bool ≝
Note: See TracChangeset for help on using the changeset viewer.