def factorial

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

import Base

51# Mathlib/Data/Nat/Factorial/Basic (Nat.factorial_succ)
52def factorial(n: Nat) -> Nat:
53  match n:
54    case 0n:
55      1n
56    case 1n+ +p:
57      Nat.mul(1n+p, factorial(p))