Digits.Digits.append: def of bend-trace-context@0.2.0.0
Import: import bend-trace-context@0.2.0.0/src/digits.bend as Digits
Lines 95-106 of bend-trace-context@0.2.0.0/src/digits.bend: https://jend.leeeet.dev/read.txt?path=bend-trace-context@0.2.0.0/src/digits.bend&start_line=95&end_line=106

import Base

# The digits of `left` followed by those of `right`: m + n digits. Identifiers
# are built from source words this way, eight digits per word.
def Digits.append(m: Nat, -n: Nat, left: Digits(m), right: Digits(n)) -> Digits(Nat.add(m, n)):
  match m:
    case 0n:
      match left:
        case DNil{}:
          right
    case 1n+p:
      match left:
        case DCon{head, tail}:
          DCon{head, Digits.append(p, n, tail, right)}

Uses (5):
  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=bend-trace-context@0.2.0.0/src/digits.bend&name=Digits
  https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/src/digits.bend&name=Digits.Con
  https://jend.leeeet.dev/definition.txt?path=bend-trace-context@0.2.0.0/src/digits.bend&name=Digits.Nil