def comb_go

bend-collections-laws-math@1.0.0.0 · src/math/natural.bend:136

import Base

136# r_{i+1} = r_i * (n - i) / (i + 1): every r_i is C(n, i), so the division
137# is exact (reference section 8.6).
138def comb_go(j: Nat, +n: Nat, +i: Nat, +r: Nat) -> Nat:
139  match j:
140    case 0n:
141      r
142    case 1n+ +jp:
143      comb_go(jp, n, 1n+i, Nat.div(Nat.mul(r, Nat.sub(n, i)), 1n+i))