Selection panel utilities

The main declaration is mkSelectionPanelRPC which helps creating rpc methods for widgets generating tactic calls based on selected sub-expressions in the main goal.

There are also some minor helper functions.

def getGoalLocations (locations : Array Lean.SubExpr.GoalsLocation) : Array Lean.SubExpr.Pos

Given a Array GoalsLocation return the array of SubExpr.Pos for all locations in the targets of the relevant goals.

Equations

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

def insertMetaVar (e : Lean.Expr) (pos : Lean.SubExpr.Pos) : Lean.MetaM Lean.Expr

Replace the sub-expression at the given position by a fresh meta-variable.

Equations

• insertMetaVar e pos = Lean.Meta.replaceSubexpr (fun (x : Lean.Expr) => Lean.Meta.mkFreshExprMVar none Lean.MetavarKind.synthetic) pos e

def String.renameMetaVar (s : String) : String

Replace all meta-variable names by "?_".

Equations

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

structure SelectInsertParams : 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.

instance instSelectInsertParamsClassSelectInsertParams : SelectInsertParamsClass SelectInsertParams

Equations

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

instance SelectInsertParams.instRpcEncodable : Lean.Server.RpcEncodable SelectInsertParams

Equations

• SelectInsertParams.instRpcEncodable = { rpcEncode := SelectInsertParams.instRpcEncodable.enc✝, rpcDecode := SelectInsertParams.instRpcEncodable.dec✝ }

instance SelectInsertParams.instToJsonRpcEncodablePacket : Lean.ToJson SelectInsertParams.RpcEncodablePacket✝

Equations

• SelectInsertParams.instToJsonRpcEncodablePacket = { toJson := SelectInsertParams.toJsonRpcEncodablePacket✝ }

instance SelectInsertParams.instFromJsonRpcEncodablePacket : Lean.FromJson SelectInsertParams.RpcEncodablePacket✝

Equations

• SelectInsertParams.instFromJsonRpcEncodablePacket = { fromJson? := SelectInsertParams.fromJsonRpcEncodablePacket✝ }

def mkSelectionPanelRPC {Params : Type} [SelectInsertParamsClass Params] (mkCmdStr : Array Lean.SubExpr.GoalsLocation → Lean.Expr → Params → Lean.MetaM (String × String × Option (String.Pos × String.Pos))) (helpMsg : String) (title : String) (onlyGoal : optParam Bool true) (onlyOne : optParam Bool false) (params : Params) : Lean.Server.RequestM (Lean.Server.RequestTask ProofWidgets.Html)

Helper function to create a widget allowing to select parts of the main goal and then display a link that will insert some tactic call.

The main argument is mkCmdStr which is a function creating the link text and the tactic call text. The helpMsg argument is displayed when nothing is selected and title is used as a panel title. The onlyGoal argument says whether the selected has to be in the goal. Otherwise it can be in the local context. The onlyOne argument says whether one should select only one sub-expression. In every cases, all selected subexpressions should be in the main goal or its local context.

The last arguments params should not be provided so that the output has type Params → RequestM (RequestTask Html) and can be fed to the mk_rpc_widget% elaborator.

Note that the pos and goalType arguments to mkCmdStr could be extracted for the Params argument but that extraction would happen in every example, hence it is factored out here. We also make sure mkCmdStr is executed in the right context.

Equations

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