Documentation

ProofWidgets.Component.HtmlDisplay

source
structure ProofWidgets.HtmlDisplayProps :
Type
Instances For
    source
    @[implicit_reducible]
    instance ProofWidgets.instRpcEncodableHtmlDisplayProps :
    Lean.Server.RpcEncodable HtmlDisplayProps
    source
    def ProofWidgets.HtmlDisplay :
    Component HtmlDisplayProps
    Instances For
      source
      def ProofWidgets.HtmlDisplayPanel :
      Component HtmlDisplayProps
      Instances For
        source
        class ProofWidgets.HtmlEval (α : Type u) :
        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
          source
          @[implicit_reducible]
          instance ProofWidgets.instHtmlEvalHtml :
          HtmlEval Html
          source
          @[implicit_reducible]
          instance ProofWidgets.instHtmlEvalHtmlOfMonadLiftTCommandElabM {m : Type → Type u_1} [MonadLiftT m Lean.Elab.Command.CommandElabM] :
          HtmlEval (m Html)
          source
          @[implicit_reducible]
          instance ProofWidgets.instHtmlEvalCoreMHtml :
          HtmlEval (Lean.CoreM Html)
          source
          @[implicit_reducible]
          instance ProofWidgets.instHtmlEvalMetaMHtml :
          HtmlEval (Lean.MetaM Html)
          source
          @[implicit_reducible]
          instance ProofWidgets.instHtmlEvalTermElabMHtml :
          HtmlEval (Lean.Elab.TermElabM Html)
          source
          unsafe def ProofWidgets.HtmlCommand.evalCommandMHtmlUnsafe (stx : Lean.Term) :
          Lean.Elab.TermElabM (Lean.Elab.Command.CommandElabM Html)
          Instances For
            source
            @[implemented_by ProofWidgets.HtmlCommand.evalCommandMHtmlUnsafe]
            opaque ProofWidgets.HtmlCommand.evalCommandMHtml :
            Lean.Term → Lean.Elab.TermElabM (Lean.Elab.Command.CommandElabM Html)
            source
            def ProofWidgets.HtmlCommand.htmlCmd :
            Lean.ParserDescr

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

            Instances For
              source
              def ProofWidgets.HtmlCommand.elabHtmlCmd :
              Lean.Elab.Command.CommandElab
              Instances For
                source
                def Lean.MessageData.ofHtml (h : ProofWidgets.Html) (alt : String) :
                CoreM MessageData

                Construct a structured message from ProofWidgets HTML.

                For the meaning of alt, see MessageData.ofWidget.

                Instances For