Conv widget

This is a slightly improved version of one of the examples that used to be 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 Mathlib.Tactic.Conv.insertEnterSyntax (locations : Array Lean.SubExpr.GoalsLocation) (goalType : Lean.Expr) : Lean.MetaM Lean.Syntax

Return the syntax to insert for the conv widget. Factored out of insertEnter for easy testing.

Equations

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

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

Return the text for the link in the conv widget that inserts the replacement, and also return the replacement, and the range within the file to highlight after the replacement is inserted. The highlighted range will always be the trailing skip.

Equations

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

def Mathlib.Tactic.Conv.SelectionPanel.rpc (params : SelectInsertParams) : Lean.Server.RequestM (Lean.Server.RequestTask ProofWidgets.Html)

Rpc function for the conv widget.

Equations

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

def Mathlib.Tactic.Conv.SelectionPanel : ProofWidgets.Component SelectInsertParams

The conv widget.

Equations

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

def Mathlib.Tactic.Conv.tacticConv? : Lean.ParserDescr

Display a widget panel allowing to generate a conv call zooming to the subexpression selected in the goal or in the type of a local hypothesis or let-decl.

Equations

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