Elaborators for writing ProofWidgets.Html trees using the HTML-like syntax defined in Lean.Data.Html.Syntax.

def ProofWidgets.«jsx%» : Lean.Parser.Parser

A ProofWidgets.Html literal written using HTML-like syntax.

The HTML-like syntax is defined in core Lean (Lean.Data.Html.Syntax). The following behavior is specific to ProofWidgets:

• Lowercase tags are interpreted as standard HTML elements, whereas uppercase tags are expected to be ProofWidgets.Components.

• Attributes on an HTML element have type String × Json (name and value) rather than String × String.

• Attributes on a widget component of type ProofWidgets.Component Props are the fields of Props. They can be specified as interpolated values <Widget name={val}/> and whole structures <Widget {... { name := val }}/>. Interpolation of single attributes with <Widget {("name", val)}/> is not supported on components.

• At most one node is allowed between the braces, and this must be known statically, so e.g. jsx%{<br/><br/>} and jsx%{{... hs}} are forbidden.

Equations

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