def groups_of

mlbend-generative@0.1.1.0 · main.bend:275

import Base

275# How many entries the walk emits over n entries. The count recurses on
276# the count left, exactly as the walk recurses on the list left, and the
277# two matches (on the count, on the skip) are in the same order — that
278# is what lets the law below follow both by induction.
279def groups_of(+n: Nat, +k: Nat, +skip: Nat) -> Nat:
280  match n:
281    case 0n:
282      0n
283    case 1n+m:
284      match skip:
285        case 0n:
286          (1n + groups_of(m, k, Nat.sub(k, 1n)) : Nat)
287        case 1n+r:
288          groups_of(m, k, r)