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.

Equations

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

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

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

Equations

• Std.CodeAction.mkHoleCodeAction n = do let __discr ← read match __discr with | { env := env, opts := opts } => liftM (IO.ofExcept (Std.CodeAction.mkHoleCodeAction.impl✝ n env opts))

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.

Equations

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

@[inline, reducible]

abbrev Std.CodeAction.TacticSeqCodeAction : Type

A tactic code action extension.

Equations

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

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

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

Equations

• Std.CodeAction.mkTacticCodeAction n = do let __discr ← read match __discr with | { env := env, opts := opts } => liftM (IO.ofExcept (Std.CodeAction.mkTacticCodeAction.impl✝ n env opts))

def Std.CodeAction.mkTacticSeqCodeAction (n : Lean.Name) : Lean.ImportM Std.CodeAction.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.

structure Std.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 Std.CodeAction.instInhabitedTacticCodeActionEntry : Inhabited Std.CodeAction.TacticCodeActionEntry

Equations

• Std.CodeAction.instInhabitedTacticCodeActionEntry = { default := { declName := default, tacticKinds := default } }

structure Std.CodeAction.TacticCodeActions : Type

The state of the tactic code actions extension.

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

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

Equations

• Std.CodeAction.instInhabitedTacticCodeActions = { default := { onAnyTactic := default, onTactic := default } }

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.

Equations

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

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.

Equations

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

@[inline, reducible]

abbrev Std.CodeAction.CommandCodeAction : Type

A command code action extension.

Equations

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

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

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

Equations

• Std.CodeAction.mkCommandCodeAction n = do let __discr ← read match __discr with | { env := env, opts := opts } => liftM (IO.ofExcept (Std.CodeAction.mkCommandCodeAction.impl✝ n env opts))

structure Std.CodeAction.CommandCodeActionEntry : Type

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

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

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

Equations

• Std.CodeAction.instInhabitedCommandCodeActionEntry = { default := { declName := default, cmdKinds := default } }

structure Std.CodeAction.CommandCodeActions : Type

The state of the command code actions extension.

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

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

Equations

• Std.CodeAction.instInhabitedCommandCodeActions = { default := { onAnyCmd := default, onCmd := default } }

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.

Equations

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

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.

Equations

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