law nth_set_other

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

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

234law nth_set_other:
235  for -T: Data
236  for xs: List<&2, T>
237  for k: Nat
238  for m: Nat
239  for v: T
240  for f: T
241  for h: {Nat.is_eq(k, m) == False{} : Bool}
242  {A.Arrays.nth(T, List.set(&2, T, xs, k, v), m, f) == A.Arrays.nth(T, xs, m, f) : T}

Uses (11)

Used by (0)

No other definition uses this definition.