Def Mathlib.Linter.isInLibraryRoot

Modification history

2026-10-21 00:36
Mathlib/Tactic/Linter/Header.lean
feat(Tactic/Linter/Header): access library root without cwd (#45061) …
Modified Mathlib.Linter.isInLibraryRootView on Github →
2026-04-29 03:39
Mathlib/Tactic/Linter/Header.lean
feat(Tactic/Linter/Header): make header linter work downstream (#38396) …
Added Mathlib.Linter.isInLibraryRootView on Github →