def Lean.Html.render (h : Html) : String

Renders into a string to be consumed by browsers. The input's structure is respected as much as possible:

• No whitespace is added or removed.

• Tag names are not escaped.

The output uses HTML5 syntax. It is not compatible with XML syntax for HTML.

Details of the output syntax

We make the following XML-compatible choices:

• Void elements with isEmpty children are rendered as self-closing tags.

  • Void elements with non-isEmpty children are rendered like normal elements. Such elements are forbidden by the HTML spec.

• Attribute values are always double-quoted.

And the following incompatible choices:

• Attributes with empty values are minimized.

Equations

• h.render = Lean.Html.render.go✝ "" { kinds := #[Lean.Html.RenderWorkItemKind.html✝], htmls := #[h], strs := #[] }