law index_wrap

bend-osdev-array@0.1.0.1 · LAWS.bend:139

import Base
import bend-osdev-array@0.1.0.1/array.bend as A

139law index_wrap:
140  for d: Nat
141  for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
142  for k: Nat
143  for hk: {Nat.is_lt(k, A.Arrays.slots(d)) == True{} : Bool}
144  {A.Arrays.index(d, U32.from_nat(Nat.add(A.Arrays.slots(d), k))) == k : Nat}