def join

bend-collections-laws-crypto@1.0.0.0 · spec/lib/numeric.bend:94

import Base

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