Code action for @[deprecated] replacements

This is an opt-in mechanism for making machine-applicable @[deprecated] definitions. When enabled (by setting the machineApplicableDeprecated tag attribute), a code action will be triggered whenever the deprecation lint also fires, allowing the user to replace the usage of the deprecated constant.

opaque Batteries.machineApplicableDeprecated : Lean.TagDeclarationExtension

An environment extension for identifying @[deprecated] definitions which can be auto-fixed

def Batteries.CodeAction.deprecatedCodeActionProvider : Lean.Server.CodeActionProvider

A code action which applies replacements for @[deprecated] definitions.

Equations

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