Def Mathlib.Linter.isInMathlib

Modification history

2026-04-29 03:39
Mathlib/Tactic/Linter/Header.lean
feat(Tactic/Linter/Header): make header linter work downstream (#38396) …
Deleted Mathlib.Linter.isInMathlibView on Github →
2024-11-11 15:53
Mathlib/Tactic/Linter/Header.lean
fix: silence the linter in files not imported by `Mathlib.lean` (#18033) …
Added Mathlib.Linter.isInMathlibView on Github →