Commit 2025-04-13 18:41 9f26568c
View on Github →feat: a linter to deprecate imported modules (#20987) Writing
import Bar1
import Bar2
deprecated_module since yyyy-mm-dd
in file A.lean means that any file that imports A will have import A flagged with a suggestion to import Bar1 and Bar2 instead.
Zulip discussion