Def Mathlib.Linter.broadImportsCheck

Modification history

2024-11-07 03:11
Mathlib/Tactic/Linter/Header.lean
feat: rewrite the duplicateImports linter (#17555) …
Deleted Mathlib.Linter.broadImportsCheckView on Github →
2024-10-24 22:41
Mathlib/Tactic/Linter/Header.lean
feat: extend the linter against broad imports (#14898) …
Modified Mathlib.Linter.broadImportsCheckView on Github →
2024-10-16 03:00
Mathlib/Tactic/Linter/Header.lean
feat: the header linter (#16574) …
Added Mathlib.Linter.broadImportsCheckView on Github →