105 open Hints_declaration
127 (** val z_of_offset : Pointers.offset -> Z.z **)
128 let z_of_offset ofs =
129 BitVectorZ.z_of_unsigned_bitvector Pointers.offset_size (Pointers.offv ofs)
131 (** val shiftn : Pointers.offset -> Nat.nat -> Pointers.offset **)
132 let rec shiftn off = function
136 (Pointers.shift_offset (Nat.S (Nat.S Nat.O)) off
137 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S Nat.O)) (Nat.S Nat.O))) n