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

    Rpc function for the congrm widget.

    Equations
    Instances For

      The congrm widget.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

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

        Equations
        Instances For