Documentation

Mathlib.Tactic.Widget.Calc

Calc widget #

This file redefines the calc tactic so that it displays a widget panel allowing to create new calc steps with holes specified by selected sub-expressions in the goal.

Code action to create a calc tactic from the current goal.

Equations
  • One or more equations did not get rendered due to their size.
  • createCalc _params _snap ctx _stack node = pure #[]
Instances For

    Parameters for the calc widget.

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

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

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

        Rpc function for the calc widget.

        Equations
        Instances For

          The calc widget.

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