Myers.band_step.updated: def of bend-edit-distance@0.2.2.0
Import: import bend-edit-distance@0.2.2.0/src/Myers.bend as Myers
Lines 325-338 of bend-edit-distance@0.2.2.0/src/Myers.bend: https://jend.leeeet.dev/read.txt?path=bend-edit-distance@0.2.2.0/src/Myers.bend&start_line=325&end_line=338

import Base

def band_step.updated(updated: UpdatedBand, rest: List<&2, Peq>, +first: Nat,
                      symbol: U32, +length: Nat, +target_length: Nat,
                      +column: Nat, maximum: Nat, padding: Nat) -> BandStep:
  match updated:
    case UpdatedBand{entries, +score, carry, +bottom}:
      # Completing the suffix by edits bounds the optimum. Padding can lower
      # the stored bottom score, so add it back before tightening k.
      +k = Nat.min(maximum, Nat.add(U32.to_nat(score),
        Nat.add(Nat.max(Nat.sub(target_length, column), Nat.sub(length, bottom)),
          Bool.pick(Nat, Nat.is_ge(bottom, length), padding, 0n))))
      work = Nat.sub(Nat.div(bottom, 32n), first)
      expand_band(entries, rest, score, carry, symbol, first, k, length, target_length,
        column, work, Nat.is_le(Nat.add(Nat.add(bottom, U32.to_nat(score)), target_length),
          Nat.add(Nat.add(Nat.add(k, length), column), 62n)))

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.pick
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_ge
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.max
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.min
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-edit-distance@0.2.2.0/src/Myers.bend&name=BandStep
  https://jend.leeeet.dev/definition.txt?path=bend-edit-distance@0.2.2.0/src/Myers.bend&name=Peq
  https://jend.leeeet.dev/definition.txt?path=bend-edit-distance@0.2.2.0/src/Myers.bend&name=UpdatedBand
  https://jend.leeeet.dev/definition.txt?path=bend-edit-distance@0.2.2.0/src/Myers.bend&name=expand_band