# CongrM widget #

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

### CongrM widget #

source
def makeCongrMString (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 congrm widget.

Equations

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

Instances For

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

Rpc function for the congrm widget.

Equations

- CongrMSelectionPanel.rpc = mkSelectionPanelRPC makeCongrMString "Use shift-click to select sub-expressions in the goal that should become holes in congrm." "CongrM 🔍"

Instances For

source
def CongrMSelectionPanel :
ProofWidgets.Component SelectInsertParams

The congrm widget.

Equations

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

Instances For

source
def tacticCongrm? :
Lean.ParserDescr

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

Equations

- tacticCongrm? = Lean.ParserDescr.node `tacticCongrm? 1024 (Lean.ParserDescr.nonReservedSymbol "congrm?" false)

Instances For