law swap_old

lawful-arrays@0.1.0.0 · LAWS.bend:136

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

136law swap_old:
137  for -T: Data
138  for a: Array<T>
139  for d: Nat
140  for i: U32
141  for v: T
142  for hf: {D.full(T, a, d) == True{} : Bool}
143  for hd: {Nat.is_lt(d, 32n) == True{} : Bool}
144  {Some{Pair.snd(Array<T>, T, Array.swap(T, a, i, v))} == List.get(&2, T, D.view(T, a), D.slot(i, d)) : Maybe<&2, T>}