term_! — Mathlib

Lean4
/-- factorial notation `(n)!` for `Nat.factorial n`.
In Lean, names can end with exclamation marks (e.g. `List.get!`), so you cannot write
`n!` in Lean, but must write `(n)!` or `n !` instead. The former is preferred, since
Lean can confuse the `!` in `n !` as the (prefix) Boolean negation operation in some
cases.
For numerals the parentheses are not required, so e.g. `0!` or `1!` work fine.
Todo: replace occurrences of `n !` with `(n)!` in Mathlib. -/
@[scoped term_parser 1000]
public meta def term_! : Lean.TrailingParserDescr✝ :=
  ParserDescr.trailingNode✝ `Nat.term_! 10000 0 (ParserDescr.symbol✝ "!")
Похожие утверждения