Def Mathlib.Linter.DirectoryDependency.forbiddenImportDirs

Modification history

2026-09-19 13:56
Mathlib/Tactic/Linter/DirectoryDependency.lean
chore(Linter/DirectoryDependency): move forbidden directories into a JSON file (#41938)
Modified Mathlib.Linter.DirectoryDependency.forbiddenImportDirsView on Github →
2025-03-31 05:22
Mathlib/Tactic/Linter/DirectoryDependency.lean
feat(Tactic/Linter): a linter for directory dependencies (#23088) …
Added Mathlib.Linter.DirectoryDependency.forbiddenImportDirsView on Github →