Fast.append.words: def of lawful-bytes@0.1.1.0
Import: import lawful-bytes@0.1.1.0/fast.bend as Fast
Lines 111-120 of lawful-bytes@0.1.1.0/fast.bend: https://jend.leeeet.dev/read.txt?path=lawful-bytes@0.1.1.0/fast.bend&start_line=111&end_line=120

import Base

# n words to dst from word di on, taken from src's bytes at a shift of sh
# bits: lo is src word si, r holds word si + 1.
def append.words(n: Nat, r: Array<U32> & U32, +lo: U32, dst: Array<U32>, +si: U32, +di: U32, +sh: Nat) -> Array<U32> & Array<U32>:
  match n:
    case 0n:
      (src, w) = r
      (dst, src)
    case 1n+k:
      (src, +hi) = r
      append.words(k, Array.get(U32, src, (si + 2 : U32)), hi, Array.set(U32, dst, di, (U32.shrn(lo, sh) .|. U32.shln(hi, Nat.sub(32n, sh)) : U32)), (si + 1 : U32), (di + 1 : U32), sh)

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.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=Nat.sub
  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
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shln
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shrn