Def Mathlib.Linter.DupNamespaceLinter.getIds

Modification history

2024-10-18 01:51

Mathlib/Tactic/Linter/Lint.lean

feat(Tactic/Linter/Lint): improve `dupNamespace` linter (#17631) …

Deleted Mathlib.Linter.DupNamespaceLinter.getIds View on Github →

2024-03-29 04:50

Mathlib/Tactic/Lint.lean

feat: `dupNamespace` as a syntax linter (#11154) …

Added Mathlib.Linter.DupNamespaceLinter.getIds View on Github →