Def Mathlib.Linter.DeprecatedModule.deprecated.moduleLinter

Modification history

2026-05-29 13:23

Mathlib/Tactic/Linter/DeprecatedModule.lean

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

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

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 →