Def Mathlib.Linter.getImports

Modification history

2026-09-01 18:09
Mathlib/Tactic/Linter/Header.lean
perf(Tactic/Linter/Header): different implementation for header linter (#40347) …
Deleted Mathlib.Linter.getImportsView on Github →
2025-12-18 04:36
Mathlib/Tactic/Linter/Header.lean
fix(Linter): deprecated module linter now fires for public/meta imports (#32422) …
Added Mathlib.Linter.getImportsView on Github →