def SwapW

lawful-arrays@0.1.0.0 · proof_shape.bend:39

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

39# Array.swap.go(a, ...) is (na, old) with na as perfect as a at every depth.
40def SwapW(-T: Type, -a: Array<T>, -n: U32, -i: U32, -v: T, -z: Bool, -d: Nat) -> Type:
41  &na:Array<T> -> &old:T -> {Array.swap.go(T, a, n, i, v, z) == (na, old) : Array<T> & T}
42    & {D.full(T, na, d) == D.full(T, a, d) : Bool}