type SwapFull

bendtorch-core@0.1.0.0 · src/storage/refinement.bend:321

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/array.bend as Core

321type SwapFull<-T: Data, -d: Nat, -original: Array<T>, -i: U32, -new: T> is Type:
322  SwapFull{array: Array<T>, old: T,
323    equal: {(array, old) == Array.swap(T, original, i, new) : Array<T> & T},
324    written: {array == Core.write_path(T, d, original, route(d, i), new) : Array<T>},
325    observed: {Some{old} == Model.observe(T, d, original, route(d, i)) : Maybe<&2, T>},
326    balanced: Model.Balanced(T, d, array)}