Def Mathlib.Linter.directoryDependencyCheck

Modification history

2025-05-28 07:47
Mathlib/Tactic/Linter/DirectoryDependency.lean
feat(Tactic/Linter/DirectoryDependency): add an allow-list for directories with few imports (#24109) …
Modified Mathlib.Linter.directoryDependencyCheckView on Github →
2025-03-31 05:22
Mathlib/Tactic/Linter/DirectoryDependency.lean
feat(Tactic/Linter): a linter for directory dependencies (#23088) …
Added Mathlib.Linter.directoryDependencyCheckView on Github →