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

opaque Lean.Linter.deprecatedAttr : Lean.ParametricAttribute (Option Lake.Name)

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

Equations

• Lean.Linter.isDeprecated env declName = Option.isSome (Lean.ParametricAttribute.getParam? Lean.Linter.deprecatedAttr env declName)

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

Equations

• Lean.MessageData.isDeprecationWarning msg = Lean.MessageData.hasTag (fun (x : Lake.Name) => x == `Lean.Linter.deprecatedAttr) msg

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

Equations

• Lean.Linter.getDeprecatedNewName env declName = Option.getD (Lean.ParametricAttribute.getParam? Lean.Linter.deprecatedAttr env declName) none

def Lean.Linter.checkDeprecated {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadLog m] [Lean.AddMessageContext m] [Lean.MonadOptions m] (declName : Lake.Name) : m Unit

Equations

• One or more equations did not get rendered due to their size.