Documentation

Lean.Widget.InteractiveCode

RPC infrastructure for storing and formatting code fragments, in particular Exprs, with environment and subexpression information.

A tag indicating the diff status of the expression. Used when showing tactic diffs.

Instances For

Information about a subexpression within delaborated code.

  • The Elab.Info node with the semantics of this part of the output.

  • subexprPos : Lean.SubExpr.Pos

    The position of this subexpression within the top-level expression. See Lean.SubExpr.

  • 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 git diff).

Instances For
@[reducible, inline]

Pretty-printed syntax (usually but not necessarily an Expr) with embedded Infos.

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

Tags pretty-printed code with infos from the delaborator.

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