Documentation

Mathlib.Tactic.Widget.GCongr

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
🔸 coverage
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.

Instances For
    source
    🔸 coverage
    def GCongrSelectionPanel.rpc (params : SelectInsertParams) :
    Lean.Server.RequestM (Lean.Server.RequestTask ProofWidgets.Html)

    Rpc function for the gcongr widget.

    Instances For
      source
      🔸 coverage
      def GCongrSelectionPanel :
      ProofWidgets.Component SelectInsertParams

      The gcongr widget.

      Instances For
        source
        🔸 coverage
        def tacticGcongr? :
        Lean.ParserDescr

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

        Instances For