Def Mathlib.Linter.getAliasSyntax

Modification history

2024-10-18 01:51
Mathlib/Tactic/DeclarationNames.lean
feat(Tactic/Linter/Lint): improve `dupNamespace` linter (#17631) …
Added Mathlib.Linter.getAliasSyntaxView on Github →