addModuleDeprecation — Mathlib

Lean4
/-- `addModuleDeprecation` adds to the `deprecatedModuleExt` extension the pair consisting of the
current module name and the array of its direct imports.

It ignores the `Init` import, since this is a special module that is expected to be imported
by all files.

It also ignores the `Mathlib/Tactic/Linter/DeprecatedModule.lean` import (namely, the current file),
since there is no need to import this module.
-/
def addModuleDeprecation {m : Type → Type} [Monad m] [MonadEnv m] (msg? : Option String) : m Unit := do
  let modName ← getMainModule
  modifyEnv
      (deprecatedModuleExt.addEntry ·
        (modName,
          (← getEnv).imports.filterMap fun i ↦
            if i.module == `Init || i.module == `Mathlib.Tactic.Linter.DeprecatedModule then none else i.module,
          msg?))
Похожие утверждения