# Initial setup for code action attributes #

- `@[hole_code_action]` and `@[command_code_action]` now live in the Lean repository, and are builtin.

- Attribute `@[tactic_code_action]` collects code actions which will be called on each occurrence of a tactic.

source
@[reducible, inline]
abbrev Batteries.CodeAction.TacticCodeAction :
Type

A tactic code action extension.

Equations

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

Instances For

source
@[reducible, inline]
abbrev Batteries.CodeAction.TacticSeqCodeAction :
Type

A tactic code action extension.

Equations

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

Instances For

source
def Batteries.CodeAction.mkTacticCodeAction (n : Lean.Name) :
Lean.ImportM TacticCodeAction

Read a tactic code action from a declaration of the right type.

Equations

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

Instances For

source
def Batteries.CodeAction.mkTacticSeqCodeAction (n : Lean.Name) :
Lean.ImportM TacticSeqCodeAction

Read a tacticSeq code action from a declaration of the right type.

Equations

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

Instances For

source
structure Batteries.CodeAction.TacticCodeActionEntry :
Type

An entry in the tactic code actions extension, containing the attribute arguments.

- declName : Lean.Name

  The declaration to tag

- tacticKinds : Array Lean.Name

  The tactic kinds that this extension supports. If empty it is called on all tactic kinds.

Instances For

source
instance Batteries.CodeAction.instInhabitedTacticCodeActionEntry :
Inhabited TacticCodeActionEntry
Equations

- Batteries.CodeAction.instInhabitedTacticCodeActionEntry = { default := Batteries.CodeAction.instInhabitedTacticCodeActionEntry.default }

source
def Batteries.CodeAction.instInhabitedTacticCodeActionEntry.default :
TacticCodeActionEntry
Equations

- Batteries.CodeAction.instInhabitedTacticCodeActionEntry.default = { declName := default, tacticKinds := default }

Instances For

source
structure Batteries.CodeAction.TacticCodeActions :
Type

The state of the tactic code actions extension.

- onAnyTactic : Array TacticCodeAction

  The list of tactic code actions to apply on any tactic.

- onTactic : Lean.NameMap (Array TacticCodeAction)

  The list of tactic code actions to apply when a particular tactic kind is highlighted.

Instances For

source
instance Batteries.CodeAction.instInhabitedTacticCodeActions :
Inhabited TacticCodeActions
Equations

- Batteries.CodeAction.instInhabitedTacticCodeActions = { default := Batteries.CodeAction.instInhabitedTacticCodeActions.default }

source
def Batteries.CodeAction.instInhabitedTacticCodeActions.default :
TacticCodeActions
Equations

- Batteries.CodeAction.instInhabitedTacticCodeActions.default = { onAnyTactic := default, onTactic := default }

Instances For

source
def Batteries.CodeAction.TacticCodeActions.insert (self : TacticCodeActions) (tacticKinds : Array Lean.Name) (action : TacticCodeAction) :
TacticCodeActions

Insert a tactic code action entry into the `TacticCodeActions` structure.

Equations

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

Instances For

source
opaque Batteries.CodeAction.tacticSeqCodeActionExt :
Lean.PersistentEnvExtension Lean.Name (Lean.Name × TacticSeqCodeAction) (Array Lean.Name × Array TacticSeqCodeAction)

An extension which collects all the tactic code actions.

source
opaque Batteries.CodeAction.tacticCodeActionExt :
Lean.PersistentEnvExtension TacticCodeActionEntry (TacticCodeActionEntry × TacticCodeAction) (Array TacticCodeActionEntry × TacticCodeActions)

An extension which collects all the tactic code actions.

source
def Batteries.CodeAction.tactic_code_action :
Lean.ParserDescr

This attribute marks a code action, which is used to suggest new tactics or replace existing ones.

- `@[tactic_code_action]`: This is a code action which applies to the spaces between tactics, to suggest a new tactic to change the goal state.

- `@[tactic_code_action kind]`: This is a code action which applies to applications of the tactic `kind` (a tactic syntax kind), which can replace the tactic or insert things before or after it.

- `@[tactic_code_action kind₁ kind₂]`: shorthand for `@[tactic_code_action kind₁, tactic_code_action kind₂]`.

- `@[tactic_code_action *]`: This is a tactic code action that applies to all tactics. Use sparingly.

Equations

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

Instances For