law index_of_nat

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

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

132law index_of_nat:
133  for d: Nat
134  for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
135  for k: Nat
136  for hk: {Nat.is_lt(k, A.Arrays.slots(d)) == True{} : Bool}
137  {A.Arrays.index(d, U32.from_nat(k)) == k : Nat}