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.

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

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

    Rpc function for the gcongr widget.

    Equations
    Instances For

      The gcongr widget.

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

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

        Equations
        Instances For