def split

bend-collections-laws-math@1.0.0.0 · proofs/lib/lemmas/src/wide.bend:114

import Base

114def split(n: Nat, +m: Nat, w: Word(Nat.add(n, m))) -> Parts<n, m>:
115  match n:
116    case 0n:
117      Split{WNil{}, w}
118    case 1n+p:
119      match w:
120        case WCon{h, tail}:
121          split_cons(p, m, h, split(p, m, tail))