Def Mathlib.Linter.checkBlocklist

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.checkBlocklist View on Github →

2026-05-29 13:23

Mathlib/Tactic/Linter/DirectoryDependency.lean

chore: bump toolchain to v4.31.0-rc1 (#39980)

Added Mathlib.Linter.checkBlocklist View on Github →