law nth_set_same

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

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

225law nth_set_same:
226  for -T: Data
227  for xs: List<&2, T>
228  for k: Nat
229  for v: T
230  for f: T
231  for h: {Nat.is_lt(k, List.length(&2, T, xs)) == True{} : Bool}
232  {A.Arrays.nth(T, List.set(&2, T, xs, k, v), k, f) == v : T}