law index_of_u32

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

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

146law index_of_u32:
147  for d: Nat
148  for i: U32
149  for hi: {Nat.is_lt(U32.to_nat(i), A.Arrays.slots(d)) == True{} : Bool}
150  {A.Arrays.index(d, i) == U32.to_nat(i) : Nat}