SelectInsertParamsClass

Defines the basic class of parameters for a select and insert widget.

This needs to be in a separate file in order to initialize the deriving handler.

class SelectInsertParamsClass (α : Type) : Type

Structures providing parameters for a Select and insert widget.

• pos : α → Lean.Lsp.Position

  Cursor position in the file at which the widget is being displayed.

• goals : α → Array Lean.Widget.InteractiveGoal

  The current tactic-mode goals.

• selectedLocations : α → Array Lean.SubExpr.GoalsLocation

  Locations currently selected in the goal state.

• replaceRange : α → Lean.Lsp.Range

  The range in the source document where the command will be inserted.

def Lean.Elab.mkSelectInsertParamsInstanceHandler (declNames : Array Lean.Name) : Lean.Elab.Command.CommandElabM Bool

Handler deriving a SelectInsertParamsClass instance.

Equations

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