Def Mathlib.Linter.modPathToRootPath

Modification history

2026-10-21 00:36

Mathlib/Tactic/Linter/Header.lean

feat(Tactic/Linter/Header): access library root without cwd (#45061) …

Added Mathlib.Linter.modPathToRootPath View on Github →