Documentation

ProofWidgets.Presentation.Expr

An Expr presenter is similar to a delaborator but outputs HTML trees instead of syntax, and the output HTML can contain elements which interact with the original Expr in some way. We call interactive outputs with a reference to the original input presentations.

  • userName : String

    A user-friendly name for this presenter. For example, "LaTeX".

  • Whether the output HTML has inline (think something which fits in the space normally occupied by an Expr, e.g. LaTeX) or block (think large diagram which needs dedicated space) layout.

Instances For

    Register an Expr presenter. It must have the type ProofWidgets.ExprPresenter.

    @[implemented_by _private.ProofWidgets.Presentation.Expr.0.ProofWidgets.evalExprPresenterUnsafe]
    Instances For
      Instances For
        @[deprecated]
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          This component shows a selection of all known and applicable ProofWidgets.ExprPresenters which are used to render the expression when selected. The one with highest precedence (TODO) is shown by default.

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