Documentation

ProofWidgets.Component.HtmlDisplay

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      class ProofWidgets.HtmlEval (α : Type u) :

      Any term t : α with a HtmlEval α instance can be evaluated in a #html t command.

      This is analogous to how Lean.MetaEval supports #eval.

      Instances
        Equations
        • ProofWidgets.instHtmlEvalHtmlOfMonadLiftTCommandElabM = { eval := monadLift }
        @[implemented_by ProofWidgets.HtmlCommand.evalCommandMHtmlUnsafe]

        Display a value of type Html in the infoview.

        The input can be a pure value or a computation in any Lean metaprogramming monad (e.g. CommandElabM Html).

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

            The html! tactic is deprecated and does nothing. If you have a use for it, please open an issue on https://github.com/leanprover-community/ProofWidgets4.

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

              Construct a structured message from ProofWidgets HTML.

              For the meaning of alt, see MessageData.ofWidget.

              Equations
              Instances For