Conv widget #
This is a slightly improved version of one of the examples in the ProofWidget library.
It defines a
conv? tactic that displays a widget panel allowing to generate
conv call zooming to the subexpression selected in the goal.
Return the link text and inserted text above and below of the conv widget.
- One or more equations did not get rendered due to their size.
Rpc function for the conv widget.