ProofIndex.tswap: def of lawful-arrays@0.1.0.0
Import: import lawful-arrays@0.1.0.0/proof_index.bend as ProofIndex
Lines 547-558 of lawful-arrays@0.1.0.0/proof_index.bend: https://jend.leeeet.dev/read.txt?path=lawful-arrays@0.1.0.0/proof_index.bend&start_line=547&end_line=558

import Base
import lawful-arrays@0.1.0.0/proof_tree.bend as P

# The tree a swap leaves, as a Tree (so the written array has a mirror too).
def tswap(-T: Data, t: P.Tree<T>, +n: U32, +i: U32, v: T, z: Bool) -> P.Tree<T>:
  match t z:
    case P.TLeaf{x} _:
      P.TLeaf{v}
    case P.TNode{l, r} True{}:
      +h = U32.shr(n)
      P.TNode{tswap(T, l, h, i, v, U32.is_lt(i, U32.shr(h))), r}
    case P.TNode{l, r} False{}:
      +h = U32.shr(n)
      +j = U32.sub(i, h)
      P.TNode{l, tswap(T, r, h, j, v, U32.is_lt(j, U32.shr(h)))}

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shr
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.sub
  https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_tree.bend&name=Tree