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

• 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

Equations

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

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

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

• 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

Equations

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

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

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.