RPC infrastructure for storing and formatting code fragments, in particular Exprs,
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.
Instances For
- The - Elab.Infonode with the semantics of this part of the output.
- subexprPos : Lean.SubExpr.PosThe position of this subexpression within the top-level expression. See Lean.SubExpr.
- diffStatus? : Option Lean.Widget.DiffTagIn 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 git diff).
Information about a subexpression within delaborated code.
Instances For
Pretty-printed syntax (usually but not necessarily an Expr) with embedded Infos.
Instances For
Instances For
Instances For
Tags pretty-printed code with infos from the delaborator.