def swap_full.go

lawful-arrays@0.1.0.0 · proof_shape.bend:150

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

150def swap_full.go(-T: Type, -a: Array<T>, +d: Nat, +i: U32, v: T, hf: {D.full(T, a, d) == True{} : Bool},
151  w: SizeW(T, a)) -> {D.full(T, Pair.fst(Array<T>, T, Array.swap(T, a, i, v)), d) == True{} : Bool}:
152  (b, +n, e, q) = w
153  %Equal.sym(Array<T> & U32, Array.size(T, a), (b, n), e) :
154    {D.full(T, Pair.fst(Array<T>, T, Array.swap.at(T, i, v, _)), d) == True{} : Bool}
155  +j = U32.and(i, U32.sub(n, 1))
156  swap_full.fin(T, a, b, n, i, v, d, hf, q, swap_w(T, b, n, j, v, U32.is_lt(j, U32.shr(n)), d))