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 #[]

Parameters for the calc widget.

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.

Rpc function for the calc widget.

Equations

The calc widget.

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