Def Mathlib.Linter.addModuleDeprecation

Modification history

2025-09-15 12:54
Mathlib/Tactic/Linter/DeprecatedModule.lean
chore: bump toolchain to v4.24.0-rc1 (#29671)
Modified Mathlib.Linter.addModuleDeprecationView on Github →
2025-04-13 18:41
Mathlib/Tactic/Linter/DeprecatedModule.lean
feat: a linter to deprecate imported modules (#20987) …
Added Mathlib.Linter.addModuleDeprecationView on Github →