def set_full.go

lawful-arrays@0.1.0.0 · proof_shape.bend:183

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

183def set_full.go(-T: Type, -a: Array<T>, +d: Nat, +i: U32, v: T, hf: {D.full(T, a, d) == True{} : Bool},
184  w: SizeW(T, a)) -> {D.full(T, Array.set(T, a, i, v), d) == True{} : Bool}:
185  (b, +n, e, q) = w
186  %Equal.sym(Array<T> & U32, Array.size(T, a), (b, n), e) :
187    {D.full(T, Array.set.fin(T, Array.swap.at(T, i, v, _)), d) == True{} : Bool}
188  +j = U32.and(i, U32.sub(n, 1))
189  set_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))