def Digits.append

bend-trace-context@0.2.0.0 · src/digits.bend:95

import Base

95# The digits of `left` followed by those of `right`: m + n digits. Identifiers
96# are built from source words this way, eight digits per word.
97def Digits.append(m: Nat, -n: Nat, left: Digits(m), right: Digits(n)) -> Digits(Nat.add(m, n)):
98  match m:
99    case 0n:
100      match left:
101        case DNil{}:
102          right
103    case 1n+p:
104      match left:
105        case DCon{head, tail}:
106          DCon{head, Digits.append(p, n, tail, right)}