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.
Parameters for the calc widget.
- pos : Lean.Lsp.Position
- replaceRange : Lean.Lsp.Range
- isFirst : Bool
Is this the first calc step?
- indent : Nat
indentation level of the calc block.
Return the link text and inserted text above and below of the calc widget.
- One or more equations did not get rendered due to their size.