Conv widget

This is a slightly improved version of one of the examples in the ProofWidget library. It defines a conv? tactic that displays a widget panel allowing to generate a conv call zooming to the subexpression selected in the goal.

def insertEnter (locations : Array Lean.SubExpr.GoalsLocation) (goalType : Lean.Expr) (params : SelectInsertParams) : Lean.MetaM (String × String × Option (String.Pos × String.Pos))

Return the link text and inserted text above and below of the conv widget.

Equations

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

def ConvSelectionPanel.rpc (params : SelectInsertParams) : Lean.Server.RequestM (Lean.Server.RequestTask ProofWidgets.Html)

Rpc function for the conv widget.

Equations

• ConvSelectionPanel.rpc = mkSelectionPanelRPC insertEnter "Use shift-click to select one sub-expression in the goal that you want to zoom on." "Conv 🔍" false true

def ConvSelectionPanel : ProofWidgets.Component SelectInsertParams

The conv widget.

Equations

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

def tacticConv? : Lean.ParserDescr

Display a widget panel allowing to generate a conv call zooming to the subexpression selected in the goal.

Equations

• tacticConv? = Lean.ParserDescr.node `tacticConv? 1024 (Lean.ParserDescr.nonReservedSymbol "conv?" false)