Def Mathlib.Linter.getImportIds

Modification history

2025-12-05 11:03
Mathlib/Tactic/Linter/Header.lean
chore(Tactic/Linters): remove `public section` (#31803) …
Deleted Mathlib.Linter.getImportIdsView on Github →
2024-10-16 03:00
Mathlib/Tactic/Linter/Header.lean
feat: the header linter (#16574) …
Added Mathlib.Linter.getImportIdsView on Github →