Commit 2024-11-13 13:21 f3b824e6

View on Github →

feat: check that every file imports Mathlib.Init (#18281) We add a text-based check to the lint-style script, that every file either (transitively) imports Mathlib.Init, or is (transitively) imported by it.

Estimated changes

Modified Mathlib/Init.lean

Modified Mathlib/Tactic/Linter/TextBased.lean

modified def Mathlib.Linter.TextBased.lintModules

Modified scripts/lint-style.lean

added def checkInitImports

added def findImports