opaque Lean.Linter.linter.deprecated : Lean.Option Bool

structure Lean.Linter.DeprecationEntry : Type

• newName? : Option Name
• text? : Option String
• since? : Option String

@[implicit_reducible]

instance Lean.Linter.instInhabitedDeprecationEntry : Inhabited DeprecationEntry

def Lean.Linter.instInhabitedDeprecationEntry.default : DeprecationEntry

opaque Lean.Linter.deprecatedAttr : ParametricAttribute DeprecationEntry

def Lean.Linter.setDeprecated {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m] (declName : Name) (entry : DeprecationEntry) : m Unit

def Lean.Linter.isDeprecated (env : Environment) (declName : Name) : Bool

def Lean.MessageData.isDeprecationWarning (msg : MessageData) : Bool

def Lean.Linter.getDeprecatedNewName (env : Environment) (declName : Name) : Option Name

def Lean.Linter.checkDeprecated (declName : Name) : MetaM Unit