GCongr widget

This file defines a gcongr? tactic that displays a widget panel allowing to generate a gcongr call with holes specified by selecting subexpressions in the goal.

def makeGCongrString (pos : Array Lean.SubExpr.GoalsLocation) (goalType : Lean.Expr) : SelectInsertParams → Lean.MetaM (String × String × Option (String.Pos × String.Pos))

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

Equations

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

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

Rpc function for the gcongr widget.

Equations

• GCongrSelectionPanel.rpc = mkSelectionPanelRPC makeGCongrString "Use shift-click to select sub-expressions in the goal that should become holes in gcongr." "GCongr 🔍" true

def GCongrSelectionPanel : ProofWidgets.Component SelectInsertParams

The gcongr widget.

Equations

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

def tacticGcongr? : Lean.ParserDescr

Display a widget panel allowing to generate a gcongr call with holes specified by selecting subexpressions in the goal.

Equations

• tacticGcongr? = Lean.ParserDescr.node `tacticGcongr? 1024 (Lean.ParserDescr.nonReservedSymbol "gcongr?" false)