Superfactorial #
This file defines the superfactorial
sf n = 1! * 2! * 3! * ... * n!
.
Main declarations #
Nat.superFactorial
: The superfactorial, denoted bysf
.
sf
notation for superfactorial
Equations
- Nat.termSf_ = Lean.ParserDescr.node `Nat.termSf_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "sf") (Lean.ParserDescr.cat `term 60))