def concat

stelliferous@0.0.2.0 · proofs/word_encoding.bend:4

import Base

4def concat(+n: Nat, +m: Nat, w: Word(n), tail: Word(m)) -> Word(Nat.add(n,m)):
5  match n:
6    case 0n:
7      match w:
8        case WNil{}:
9          tail
10    case 1n+p:
11      match w:
12        case WCon{b,rest}:
13          WCon{b,concat(p,m,rest,tail)}