Documentation

Mathlib.Tactic.Widget.Congrm

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.

Gcongr widget #

source
def makeCongrmString (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 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
    • One or more equations did not get rendered due to their size.
    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
        Instances For