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 }
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[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