structure ProofWidgets.HtmlDisplayProps : Type

• html : ProofWidgets.Html

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

Equations

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

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.instToJsonRpcEncodablePacket : Lean.ToJson ProofWidgets.ProofWidgets.HtmlDisplayProps.RpcEncodablePacket✝

Equations

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

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.

unsafe def ProofWidgets.evalHtmlUnsafe (stx : Lean.Term) : Lean.Elab.TermElabM ProofWidgets.Html

Equations

• ProofWidgets.evalHtmlUnsafe stx = let htmlT := Lean.mkConst `ProofWidgets.Html; Lean.Elab.Term.evalTerm ProofWidgets.Html htmlT stx.raw

@[implemented_by ProofWidgets.evalHtmlUnsafe]

opaque ProofWidgets.evalHtml : Lean.Term → Lean.Elab.TermElabM ProofWidgets.Html

def ProofWidgets.htmlCmd : Lean.ParserDescr

Equations

• ProofWidgets.htmlCmd = Lean.ParserDescr.node `ProofWidgets.htmlCmd 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#html ") (Lean.ParserDescr.cat `term 0))

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

Equations

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

def ProofWidgets.htmlTac : Lean.ParserDescr

Equations

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

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

Equations

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