# 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.

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

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.

Instances For

source
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 🔍"

Instances For

source
def GCongrSelectionPanel :
ProofWidgets.Component SelectInsertParams

The gcongr widget.

Equations

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

Instances For

source
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)

Instances For