RPC infrastructure for storing and formatting code fragments, in particular
with environment and subexpression information.
- wasChanged: Lean.Widget.DiffTag
- willChange: Lean.Widget.DiffTag
- wasDeleted: Lean.Widget.DiffTag
- willDelete: Lean.Widget.DiffTag
- wasInserted: Lean.Widget.DiffTag
- willInsert: Lean.Widget.DiffTag
A tag indicating the diff status of the expression. Used when showing tactic diffs.
Elab.Infonode with the semantics of this part of the output.
- subexprPos : Lean.SubExpr.Pos
The position of this subexpression within the top-level expression. See
In certain situations such as when goal states change between positions in a tactic-mode proof, we can show subexpression-level diffs between two expressions. This field asks the renderer to display the subexpression as in a diff view (e.g. red/green like
Information about a subexpression within delaborated code.