def desc

bend-collections-laws-math@1.0.0.0 · spec/math/natural.bend:59

import Base

59# n.descFactorial k: (n - k) * n.descFactorial k at k + 1
60def desc(+n: Nat, k: Nat) -> Nat:
61  match k:
62    case 0n:
63      1n
64    case 1n+ +j:
65      Nat.mul(Nat.sub(n, j), desc(n, j))