structure ProofWidgets.HtmlDisplayProps : Type

• html : ProofWidgets.Html

instance ProofWidgets.instRpcEncodableHtmlDisplayProps : Lean.Server.RpcEncodable ProofWidgets.HtmlDisplayProps

Equations

• ProofWidgets.instRpcEncodableHtmlDisplayProps = { rpcEncode := ProofWidgets.instRpcEncodableHtmlDisplayProps.enc✝, rpcDecode := ProofWidgets.instRpcEncodableHtmlDisplayProps.dec✝ }

def ProofWidgets.HtmlDisplay : ProofWidgets.Component ProofWidgets.HtmlDisplayProps

Equations

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

def ProofWidgets.HtmlDisplayPanel : ProofWidgets.Component ProofWidgets.HtmlDisplayProps

Equations

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

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.

• eval : α → Lean.Elab.Command.CommandElabM ProofWidgets.Html

instance ProofWidgets.instHtmlEvalHtml : ProofWidgets.HtmlEval ProofWidgets.Html

Equations

• ProofWidgets.instHtmlEvalHtml = { eval := fun (ht : ProofWidgets.Html) => pure ht }

instance ProofWidgets.instHtmlEvalHtmlOfMonadLiftTCommandElabM {m : Type → Type u_1} [MonadLiftT m Lean.Elab.Command.CommandElabM] : ProofWidgets.HtmlEval (m ProofWidgets.Html)

Equations

• ProofWidgets.instHtmlEvalHtmlOfMonadLiftTCommandElabM = { eval := monadLift }

instance ProofWidgets.instHtmlEvalCoreMHtml : ProofWidgets.HtmlEval (Lean.CoreM ProofWidgets.Html)

Equations

• ProofWidgets.instHtmlEvalCoreMHtml = { eval := Lean.Elab.Command.liftCoreM }

instance ProofWidgets.instHtmlEvalMetaMHtml : ProofWidgets.HtmlEval (Lean.MetaM ProofWidgets.Html)

Equations

• ProofWidgets.instHtmlEvalMetaMHtml = { eval := fun (x : Lean.MetaM ProofWidgets.Html) => Lean.Elab.Command.liftTermElabM (liftM x) }

instance ProofWidgets.instHtmlEvalTermElabMHtml : ProofWidgets.HtmlEval (Lean.Elab.TermElabM ProofWidgets.Html)

Equations

• ProofWidgets.instHtmlEvalTermElabMHtml = { eval := Lean.Elab.Command.liftTermElabM }

unsafe def ProofWidgets.HtmlCommand.evalCommandMHtmlUnsafe (stx : Lean.Term) : Lean.Elab.TermElabM (Lean.Elab.Command.CommandElabM ProofWidgets.Html)

@[implemented_by ProofWidgets.HtmlCommand.evalCommandMHtmlUnsafe]

opaque ProofWidgets.HtmlCommand.evalCommandMHtml : Lean.Term → Lean.Elab.TermElabM (Lean.Elab.Command.CommandElabM ProofWidgets.Html)

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

Equations

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

def ProofWidgets.HtmlCommand.elabHtmlCmd : Lean.Elab.Command.CommandElab

Equations

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

@[deprecated]

def ProofWidgets.HtmlCommand.htmlTac : Lean.ParserDescr

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.

def ProofWidgets.HtmlCommand.elabHtmlTac : Lean.Elab.Tactic.Tactic

Equations

• ProofWidgets.HtmlCommand.elabHtmlTac x = pure ()

def Lean.MessageData.ofHtml (h : ProofWidgets.Html) (alt : String) : Lean.CoreM Lean.MessageData

Construct a structured message from ProofWidgets HTML.

For the meaning of alt, see MessageData.ofWidget.

Equations

• Lean.MessageData.ofHtml h alt = Lean.MessageData.ofComponent ProofWidgets.HtmlDisplay { html := h } alt