Bytes.grow.go: def of lawful-bytes@0.1.1.0
Import: import lawful-bytes@0.1.1.0/bytes.bend as Bytes
Lines 56-64 of lawful-bytes@0.1.1.0/bytes.bend: https://jend.leeeet.dev/read.txt?path=lawful-bytes@0.1.1.0/bytes.bend&start_line=56&end_line=64

import Base

# Word i onwards copied into dst; r holds word i of the old block.
def grow.go(n: Nat, r: Array<U32> & U32, dst: Array<U32>, +i: U32) -> Array<U32>:
  match n:
    case 0n:
      (src, w) = r
      dst
    case 1n+k:
      (src, +w) = r
      grow.go(k, Array.get(U32, src, (i + 1 : U32)), Array.set(U32, dst, i, w), (i + 1 : U32))

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.get
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.set
  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.add