opaque Lean.Elab.linter.deprecated.arg : Lean.Option Bool

structure Lean.Elab.DeprecatedArgEntry : Type

Entry mapping an old parameter name to a new (or no) parameter for a given declaration.

• declName : Name
• oldArg : Name
• newArg? : Option Name
• text? : Option String
• since? : Option String

@[implicit_reducible]

instance Lean.Elab.instInhabitedDeprecatedArgEntry : Inhabited DeprecatedArgEntry

def Lean.Elab.instInhabitedDeprecatedArgEntry.default : DeprecatedArgEntry

@[reducible, inline]

abbrev Lean.Elab.DeprecatedArgState : Type

State: declName → (oldArg → entry)

opaque Lean.Elab.deprecatedArgExt : SimplePersistentEnvExtension DeprecatedArgEntry DeprecatedArgState

def Lean.Elab.findDeprecatedArg? (env : Environment) (declName argName : Name) : Option DeprecatedArgEntry

Look up a deprecated argument mapping for (declName, argName).

def Lean.Elab.formatDeprecatedArgMsg (entry : DeprecatedArgEntry) : MessageData

Format the deprecation warning message for a deprecated argument.