Def Mathlib.Linter.TextBased.duplicateImportsLinter

Modification history

2024-11-07 03:11
Mathlib/Tactic/Linter/TextBased.lean
feat: rewrite the duplicateImports linter (#17555) …
Deleted Mathlib.Linter.TextBased.duplicateImportsLinterView on Github →
2024-09-12 10:52
Mathlib/Tactic/Linter/TextBased.lean
feat: lint on (syntactically) duplicate imports (#16384) …
Added Mathlib.Linter.TextBased.duplicateImportsLinterView on Github →