Def Mathlib.Notation3.$(Lean.mkIdent

Modification history

2025-01-30 09:06
Mathlib/Util/Notation3.lean
feat: let `notation3` pretty print "overapplied" notations (#21239) …
Modified Mathlib.Notation3.$(Lean.mkIdentView on Github →
2023-06-02 12:48
Mathlib/Mathport/Notation.lean
feat: `notation3` delaborator generation (#4533) …
Added Mathlib.Notation3.$(Lean.mkIdentView on Github →