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.

@[reducible, inline]

abbrev Batteries.CodeAction.TacticCodeAction : Type

A tactic code action extension.

@[reducible, inline]

abbrev Batteries.CodeAction.TacticSeqCodeAction : Type

A tactic code action extension.

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

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

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

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

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.

instance Batteries.CodeAction.instInhabitedTacticCodeActionEntry : Inhabited TacticCodeActionEntry

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.

instance Batteries.CodeAction.instInhabitedTacticCodeActions : Inhabited TacticCodeActions

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

Insert a tactic code action entry into the TacticCodeActions structure.

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.

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

An extension which collects all the tactic code actions.

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.