Refinement.SwapFull: type of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
Lines 321-326 of bendtorch-core@0.1.0.0/src/storage/refinement.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/storage/refinement.bend&start_line=321&end_line=326

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

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

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.swap
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/array.bend&name=write_path
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=Balanced
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=observe
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/refinement.bend&name=route