law swap_view

lawful-arrays@0.1.0.0 · LAWS.bend:126

import Base
import lawful-arrays@0.1.0.0/defs.bend as D

126law swap_view:
127  for -T: Data
128  for a: Array<T>
129  for d: Nat
130  for i: U32
131  for v: T
132  for hf: {D.full(T, a, d) == True{} : Bool}
133  for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
134  {D.view(T, Pair.fst(Array<T>, T, Array.swap(T, a, i, v))) == List.set(&2, T, D.view(T, a), D.slot(i, d), v) : List<&2, T>}