Size.join: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/storage/size.bend as Size
Lines 18-27 of bendtorch-core@0.1.0.0/src/storage/size.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/storage/size.bend&start_line=18&end_line=27

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

def join(-T: Data, -d: Nat, -original: Array<T>, ys: Array<T>,
  child: Sized<T, d, original>, valid: Model.Balanced(T, d, ys)) ->
  Sized<T, 1n+d, ANode{original, ys}>:
  match child:
    case Sized{xs, n, retained, measured, extent, balanced}:
      Sized{ANode{xs, ys}, U32.shl(n),
        Equal.cong(Array<T>, Array<T>, x => ANode{x, ys}, xs, original, retained),
        Equal.cong(Array<T> & U32, Array<T> & U32, r => Array.size.node(T, ys, r),
          (xs, n), Array.size(T, original), measured),
        Equal.cong(U32, U32, x => U32.shl(x), n, capacity(d), extent), (balanced, valid)}

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.size
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.size.node
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  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=Base/base.bend&name=U32.shl
  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/size.bend&name=Sized
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/size.bend&name=capacity