law swap_full

lawful-arrays@0.1.0.0 · LAWS.bend:146

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

146law swap_full:
147  for -T: Type
148  for a: Array<T>
149  for d: Nat
150  for i: U32
151  for v: T
152  for hf: {D.full(T, a, d) == True{} : Bool}
153  {D.full(T, Pair.fst(Array<T>, T, Array.swap(T, a, i, v)), d) == True{} : Bool}