Numeric.join: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/spec/lib/numeric.bend as Numeric
Lines 94-102 of bend-collections-laws-math@1.0.0.0/spec/lib/numeric.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/numeric.bend&start_line=94&end_line=102

import Base

# A 64-bit word from two 32-bit limbs (low first).
def join(n: Nat, +m: Nat, a: Word(n), b: Word(m)) -> Word(Nat.add(n, m)):
  match n:
    case 0n:
      b
    case 1n+p:
      match a:
        case WCon{h, tail}:
          WCon{h, join(p, m, tail, b)}

Uses (4):
  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=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con