def swap
import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinementimport Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/size.bend as Size
352def swap(-T: Data, +d: Nat, array: Array<T>, +i: U32, new: T,
353 valid: Model.Balanced(T, d, array)) -> SwapFull<T, d, array, i, new>:
354 swap_sized(T, d, array, i, new, Size.certify(T, d, array, valid))
Uses (7)
Used by (5)
- bendtorch-core@0.1.0.0/src/storage/refinement:law_set_refines
- bendtorch-core@0.1.0.0/src/storage/refinement:law_set_balanced
- bendtorch-core@0.1.0.0/src/storage/refinement:law_swap_balanced
- bendtorch-core@0.1.0.0/src/storage/refinement:law_swap_observed
- bendtorch-core@0.1.0.0/src/storage/refinement:law_swap_refines