Initial setup for code action attributes

• Attribute @[hole_code_action] collects code actions which will be called on each occurrence of a hole (_, ?_ or sorry).

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

• Attribute @[command_code_action] collects code actions which will be called on each occurrence of a command.

@[inline, reducible]

abbrev Std.CodeAction.HoleCodeAction : Type

A hole code action extension.

def Std.CodeAction.mkHoleCodeAction (n : Lean.Name) : Lean.ImportM Std.CodeAction.HoleCodeAction

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

opaque Std.CodeAction.holeCodeActionExt : Lean.PersistentEnvExtension Lean.Name (Lean.Name × Std.CodeAction.HoleCodeAction) (Array Lean.Name × Array Std.CodeAction.HoleCodeAction)

An extension which collects all the hole code actions.

@[inline, reducible]

abbrev Std.CodeAction.TacticCodeAction : Type

A tactic code action extension.

@[inline, reducible]

abbrev Std.CodeAction.TacticSeqCodeAction : Type

A tactic code action extension.

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

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

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

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

structure Std.CodeAction.TacticCodeActionEntry : Type

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

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

instance Std.CodeAction.instInhabitedTacticCodeActionEntry : Inhabited Std.CodeAction.TacticCodeActionEntry

structure Std.CodeAction.TacticCodeActions : Type

• onAnyTactic : Array Std.CodeAction.TacticCodeAction

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

• onTactic : Lean.NameMap (Array Std.CodeAction.TacticCodeAction)

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

The state of the tactic code actions extension.

instance Std.CodeAction.instInhabitedTacticCodeActions : Inhabited Std.CodeAction.TacticCodeActions

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

Insert a tactic code action entry into the TacticCodeActions structure.

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

An extension which collects all the tactic code actions.

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

An extension which collects all the tactic code actions.

def Std.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.

@[inline, reducible]

abbrev Std.CodeAction.CommandCodeAction : Type

A command code action extension.

def Std.CodeAction.mkCommandCodeAction (n : Lean.Name) : Lean.ImportM Std.CodeAction.CommandCodeAction

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

structure Std.CodeAction.CommandCodeActionEntry : Type

• declName : Lean.Name

  The declaration to tag

• cmdKinds : Array Lean.Name

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

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

instance Std.CodeAction.instInhabitedCommandCodeActionEntry : Inhabited Std.CodeAction.CommandCodeActionEntry

structure Std.CodeAction.CommandCodeActions : Type

• onAnyCmd : Array Std.CodeAction.CommandCodeAction

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

• onCmd : Lean.NameMap (Array Std.CodeAction.CommandCodeAction)

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

The state of the command code actions extension.

instance Std.CodeAction.instInhabitedCommandCodeActions : Inhabited Std.CodeAction.CommandCodeActions

def Std.CodeAction.CommandCodeActions.insert (self : Std.CodeAction.CommandCodeActions) (tacticKinds : Array Lean.Name) (action : Std.CodeAction.CommandCodeAction) : Std.CodeAction.CommandCodeActions

Insert a command code action entry into the CommandCodeActions structure.

opaque Std.CodeAction.cmdCodeActionExt : Lean.PersistentEnvExtension Std.CodeAction.CommandCodeActionEntry (Std.CodeAction.CommandCodeActionEntry × Std.CodeAction.CommandCodeAction) (Array Std.CodeAction.CommandCodeActionEntry × Std.CodeAction.CommandCodeActions)

An extension which collects all the command code actions.

def Std.CodeAction.command_code_action : Lean.ParserDescr

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

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

• @[command_code_action kind₁ kind₂]: shorthand for @[command_code_action kind₁, command_code_action kind₂].

• @[command_code_action]: This is a command code action that applies to all commands. Use sparingly.