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

    Information about a subexpression within delaborated code.

    Instances For
      @[inline, reducible]

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

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

            Tags pretty-printed code with infos from the delaborator.

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