structure ProofWidgets.HtmlDisplayProps : Type

• html : ProofWidgets.Html

Instances For

• ProofWidgets.ProofWidgets.HtmlDisplayProps.instRpcEncodableHtmlDisplayProps

instance ProofWidgets.ProofWidgets.HtmlDisplayProps.instToJsonRpcEncodablePacket : Lean.ToJson ProofWidgets.ProofWidgets.HtmlDisplayProps.RpcEncodablePacket✝

Equations

• ProofWidgets.ProofWidgets.HtmlDisplayProps.instToJsonRpcEncodablePacket = { toJson := ProofWidgets.ProofWidgets.HtmlDisplayProps.toJsonRpcEncodablePacket✝ }

instance ProofWidgets.ProofWidgets.HtmlDisplayProps.instFromJsonRpcEncodablePacket : Lean.FromJson ProofWidgets.ProofWidgets.HtmlDisplayProps.RpcEncodablePacket✝

Equations

• ProofWidgets.ProofWidgets.HtmlDisplayProps.instFromJsonRpcEncodablePacket = { fromJson? := ProofWidgets.ProofWidgets.HtmlDisplayProps.fromJsonRpcEncodablePacket✝ }

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

Equations

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

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

Instances

• ProofWidgets.instHtmlEvalCoreMHtml
• ProofWidgets.instHtmlEvalHtml
• ProofWidgets.instHtmlEvalHtmlOfMonadLiftTCommandElabM
• ProofWidgets.instHtmlEvalMetaMHtml
• ProofWidgets.instHtmlEvalTermElabMHtml

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)

Equations

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

@[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 = match x with | 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