Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-09-12 10:52
0ca9b837
View on Github →
feat: lint on (syntactically) duplicate imports (
#16384
) Motivation: PR
#16273
Estimated changes
Modified
Mathlib/Tactic/Linter/TextBased.lean
added
def
Mathlib.Linter.TextBased.duplicateImportsLinter