law of_list_set

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

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

190law of_list_set:
191  for -T: Data
192  for +d: Nat
193  for +xs: List<&2, T>
194  for +f: T
195  for +hl: {List.length(&2, T, xs) == A.Arrays.slots(d) : Nat}
196  for +hd: {Nat.is_lt(d, 32n) == True{} : Bool}
197  for +i: U32
198  for +v: T
199  {Array.set(T, A.Arrays.of_list(T, d, xs, f), i, v) == A.Arrays.of_list(T, d, List.set(&2, T, xs, A.Arrays.index(d, i), v), f) : Array<T>}