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

source
opaque Batteries.machineApplicableDeprecated :
Lean.TagDeclarationExtension

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

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

Instances For