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

Equations

• Lean.Elab.instInhabitedDeprecatedArgEntry = { default := Lean.Elab.instInhabitedDeprecatedArgEntry.default }

def Lean.Elab.instInhabitedDeprecatedArgEntry.default : DeprecatedArgEntry

Equations

• Lean.Elab.instInhabitedDeprecatedArgEntry.default = { declName := default, oldArg := default, newArg? := default, text? := default, since? := default }

@[reducible, inline]

abbrev Lean.Elab.DeprecatedArgState : Type

State: declName → (oldArg → entry)

Equations

• Lean.Elab.DeprecatedArgState = Lean.NameMap (Lean.NameMap Lean.Elab.DeprecatedArgEntry)

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).

Equations

• Lean.Elab.findDeprecatedArg? env declName argName = do let x ← Lean.NameMap.find? (Lean.Elab.deprecatedArgExt.getState env) declName x.find? argName

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

Format the deprecation warning message for a deprecated argument.

Equations

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