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.

CongrM widget #

source
🔸 coverage
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
    Instances For
      source
      🔸 coverage
      def CongrMSelectionPanel.rpc (params : SelectInsertParams) :
      Lean.Server.RequestM (Lean.Server.RequestTask ProofWidgets.Html)

      Rpc function for the congrm widget.

      Equations
        Instances For
          source
          🔸 coverage
          def CongrMSelectionPanel :
          ProofWidgets.Component SelectInsertParams

          The congrm widget.

          Equations
            Instances For
              source
              🔸 coverage
              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