factorial 階乗の記法が衝突しないようにする例

Zulip: precedence of Nat.factorial

import Lean
import Mathlib.Data.Nat.Factorial.Basic

namespace Nat.Factorial!
open Lean Elab Term Meta

@[scoped term_elab ident]
def elabIdentFactorial : TermElab
  | stx@`($name:ident), expectedType? => do
    let view := extractMacroScopes name.getId
    let .str parent s := view.name | throwUnsupportedSyntax
    unless s.endsWith "!" do throwUnsupportedSyntax
    let normal ← Term.observing <| elabIdent stx expectedType?
    if normal matches .error .. then
      let name' := MacroScopesView.review { view with name := .str parent (s.dropRight 1) }
      let factorial ← Term.observing <| elabTerm (← `(Nat.factorial $(mkIdent name'))) expectedType?
      if factorial matches .ok .. then
        return ← Term.applyResult factorial
    Term.applyResult normal
  | _, _ => throwUnsupportedSyntax

end Factorial!

open scoped Nat.Factorial!

variable (x : Nat)
#check x ! -- x ! : ℕ
#check x!  -- x ! : ℕ
#check List.get! [1,2,3] 0 -- [1, 2, 3].get! 0 : ℕ

Start from the shown imports, especially Mathlib.Data.Nat.Factorial.Basic, and inspect how examples in the book are organized. Check the Lean snippet with the open scoped Nat.Factorial! declaration and its three #check examples; done means the example demonstrates factorial notation without conflicting with List.get!.