Def Mathlib.Linter.DeprecatedModule.deprecated.moduleLinter

Modification history

2025-04-13 18:41

Mathlib/Tactic/Linter/DeprecatedModule.lean

feat: a linter to deprecate imported modules (#20987) …

Added Mathlib.Linter.DeprecatedModule.deprecated.moduleLinter View on Github →