Def Mathlib.Linter.DirectoryDependency.forbiddenDirsPath

Modification history

2026-09-19 13:56

Mathlib/Tactic/Linter/DirectoryDependency.lean

chore(Linter/DirectoryDependency): move forbidden directories into a JSON file (#41938)

Added Mathlib.Linter.DirectoryDependency.forbiddenDirsPath View on Github →