type Swap

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

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

120type Swap<-T: Data, -d: Nat, -original: Array<T>, -n: U32, -i: U32, -z: Bool, -new: T> is Type:
121  Swap{array: Array<T>, old: T,
122    equal: {(array, old) == Array.swap.go(T, original, n, i, new, z) : Array<T> & T},
123    written: {array == Core.write_path(T, d, original, trace(d, n, i, z), new) : Array<T>},
124    observed: {Some{old} == Model.observe(T, d, original, trace(d, n, i, z)) : Maybe<&2, T>},
125    balanced: Model.Balanced(T, d, array)}