def split

stelliferous@0.0.2.0 · proofs/word_encoding.bend:158

import Base

158def split(+n: Nat, +m: Nat, w: Word(Nat.add(n,m))) -> Split<n,m>:
159  match n:
160    case 0n:
161      Parts{WNil{},w}
162    case 1n+ +p:
163      match w:
164        case WCon{b,rest}:
165          prepend(p,m,b,split(p,m,rest))