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 #

Return the link text and inserted text above and below of the congrm widget.

Equations
    Instances For

      Rpc function for the congrm widget.

      Equations
        Instances For

          The congrm widget.

          Equations
            Instances For

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

              Equations
                Instances For