Def checkInitImports

Modification history

2024-11-13 13:21
scripts/lint-style.lean
feat: check that every file imports Mathlib.Init (#18281) …
Added checkInitImportsView on Github →