The Lean Language Reference

26.2. HTML🔗

The Html type represents HTML content. It is accessed by importing Lean.Data.Html.Basic.

🔗inductive type
Lean.Html : Type
Lean.Html : Type

HTML content, which may be either a single node or a sequence of sibling nodes.

This type is optimized for convenient authoring of HTML documents. It is not formally related to the HTML DOM representation. It is analogous to React's Fragment.

Constructors

Lean.Html.element (tag : String)
  (attrs : Array (String × String)) (children : Html) : Html

An element with the given tag name, attributes, and children.

Lean.Html.text : String → Html

Textual content.

The characters &, <, and > are always escaped to HTML entities during rendering. Use raw in raw text elements (script and style) instead.

Lean.Html.raw : String → Html

Characters to be copied verbatim (and not escaped) during rendering.

Lean.Html.seq : Array Html → Html

A sequence of HTML values.

Because this inductive type includes a sequence constructor, its values are multi-rooted HTML forests rather than single-rooted trees. This is convenient for grouping content, as in Html.seq #[.text "Paragraph.", .element "br" #[] .empty], but also introduces redundancy. The empty HTML forest, for example, is denoted by Html.seq #[], by Html.seq #[Html.seq #[]], and by infinitely many other expressions. To counter this, Html.isEmpty recognizes any input that renders to the empty string, not just the simplest one. In general, functions that consume Html should handle all possible forms of their input.

🔗def
Lean.Html.isEmpty : Html → Bool
Lean.Html.isEmpty : Html → Bool

Whether this HTML is rendered as the empty string.

Furthermore, to improve representation efficiency, functions that produce Html may simplify it on a best-effort basis. For example, Html.append merges Html.seq nodes.

🔗def
Lean.Html.append : Html → Html → Html
Lean.Html.append : Html → Html → Html

Appends two HTML forests.

Smart constructors such as Html.ofCollection, Html.ofArray, and Html.ofList also simplify in this way, so should be preferred over Html.seq.

🔗def
Lean.Html.ofCollection.{w} {ρ : Type w} [ForIn Id ρ Html] (hs : ρ) :
  Html
Lean.Html.ofCollection.{w} {ρ : Type w}
  [ForIn Id ρ Html] (hs : ρ) : Html

Merges a collection of HTML values by appending them.

Like seq (ForIn.toArray hs), but may produce a more compact representation.

🔗def
Lean.Html.ofArray (hs : Array Html) : Html
Lean.Html.ofArray (hs : Array Html) : Html

Merges an array of HTML values by appending them.

Like seq, but may produce a more compact representation.

🔗def
Lean.Html.ofList (hs : List Html) : Html
Lean.Html.ofList (hs : List Html) : Html

Merges a list of HTML values by appending them.

Like seq hs.toArray, but may produce a more compact representation.

26.2.1. Rendering🔗

The render function, defined in the Lean.Data.Html.Printer module, turns HTML values into strings that can be parsed by browsers.

🔗def
Lean.Html.render (h : Html) : String
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:

26.2.2. Literal Syntax🔗

HTML literal notation can be accessed by importing Lean.Data.Html. These literals are written inside html%{} delimiters, and elaborate to Html values.

syntaxHTML Terms
term ::= ...
    | An HTML literal. html%{A sequence of HTML content nodes:
`text` contents, `comment`s, elements,
single-item `interp`olations `{ term }`,
and many-item interpolations `{... term }` \(see `interpMany`\). content}
An HTML literal
ofArray #[text "Hello, ", element "b" #[] (ofArray #[text "world"]), text "!"] : Html#check html%{Hello, <b>world</b>!}
Live ↪

HTML content is a sequence of zero or more content items.

syntaxHTML Content Item
contentItem ::=
      text
    | An [HTML comment](https://html.spec.whatwg.org/dev/syntax.html#comments). <!-- comment -->
    | An HTML element:
`<tag attr*/>` or `<tag attr*>content</tag>`.

Tags must be closed: void element syntax such as `<br>`,
and implied end tags such as `<ul><li>item</ul>`,
are not supported. <An [HTML tag name](https://html.spec.whatwg.org/dev/syntax.html#syntax-tag-name):
an ASCII letter followed by characters other than ASCII whitespace, U+0000 NULL, `/`, `>`.
This includes [custom element names](https://html.spec.whatwg.org/dev/custom-elements.html#valid-custom-element-name). tagName An [HTML attribute](https://html.spec.whatwg.org/dev/syntax.html#attributes-2).
We support double-quoted attribute values `<tag name="val">`,
empty attributes `<tag name>`,
interpolations of one value `<tag name={ term }>`,
and interpolations of a sequence of attributes `<tag {... term }/>`.
Character references are decoded in double-quoted values. An [HTML attribute name](https://html.spec.whatwg.org/dev/syntax.html#attributes-2).
Attribute names may not start with `{` \(which would conflict with interpolation\). attr*>A sequence of HTML content nodes:
`text` contents, `comment`s, elements,
single-item `interp`olations `{ term }`,
and many-item interpolations `{... term }` \(see `interpMany`\). content</An [HTML tag name](https://html.spec.whatwg.org/dev/syntax.html#syntax-tag-name):
an ASCII letter followed by characters other than ASCII whitespace, U+0000 NULL, `/`, `>`.
This includes [custom element names](https://html.spec.whatwg.org/dev/custom-elements.html#valid-custom-element-name). tagName>
    | An HTML element:
`<tag attr*/>` or `<tag attr*>content</tag>`.

Tags must be closed: void element syntax such as `<br>`,
and implied end tags such as `<ul><li>item</ul>`,
are not supported. <An [HTML tag name](https://html.spec.whatwg.org/dev/syntax.html#syntax-tag-name):
an ASCII letter followed by characters other than ASCII whitespace, U+0000 NULL, `/`, `>`.
This includes [custom element names](https://html.spec.whatwg.org/dev/custom-elements.html#valid-custom-element-name). tagName An [HTML attribute](https://html.spec.whatwg.org/dev/syntax.html#attributes-2).
We support double-quoted attribute values `<tag name="val">`,
empty attributes `<tag name>`,
interpolations of one value `<tag name={ term }>`,
and interpolations of a sequence of attributes `<tag {... term }/>`.
Character references are decoded in double-quoted values. An [HTML attribute name](https://html.spec.whatwg.org/dev/syntax.html#attributes-2).
Attribute names may not start with `{` \(which would conflict with interpolation\). attr*/>
    | {term}
    | {...term}
syntaxHTML Attribute
An [HTML attribute](https://html.spec.whatwg.org/dev/syntax.html#attributes-2).
We support double-quoted attribute values `<tag name="val">`,
empty attributes `<tag name>`,
interpolations of one value `<tag name={ term }>`,
and interpolations of a sequence of attributes `<tag {... term }/>`.
Character references are decoded in double-quoted values. attr ::=
      An [HTML attribute](https://html.spec.whatwg.org/dev/syntax.html#attributes-2).
We support double-quoted attribute values `<tag name="val">`,
empty attributes `<tag name>`,
interpolations of one value `<tag name={ term }>`,
and interpolations of a sequence of attributes `<tag {... term }/>`.
Character references are decoded in double-quoted values. An [HTML attribute name](https://html.spec.whatwg.org/dev/syntax.html#attributes-2).
Attribute names may not start with `{` \(which would conflict with interpolation\). attrName=str
    | An [HTML attribute](https://html.spec.whatwg.org/dev/syntax.html#attributes-2).
We support double-quoted attribute values `<tag name="val">`,
empty attributes `<tag name>`,
interpolations of one value `<tag name={ term }>`,
and interpolations of a sequence of attributes `<tag {... term }/>`.
Character references are decoded in double-quoted values. An [HTML attribute name](https://html.spec.whatwg.org/dev/syntax.html#attributes-2).
Attribute names may not start with `{` \(which would conflict with interpolation\). attrName={term}
    | An [HTML attribute](https://html.spec.whatwg.org/dev/syntax.html#attributes-2).
We support double-quoted attribute values `<tag name="val">`,
empty attributes `<tag name>`,
interpolations of one value `<tag name={ term }>`,
and interpolations of a sequence of attributes `<tag {... term }/>`.
Character references are decoded in double-quoted values. An [HTML attribute name](https://html.spec.whatwg.org/dev/syntax.html#attributes-2).
Attribute names may not start with `{` \(which would conflict with interpolation\). attrName
    | An [HTML attribute](https://html.spec.whatwg.org/dev/syntax.html#attributes-2).
We support double-quoted attribute values `<tag name="val">`,
empty attributes `<tag name>`,
interpolations of one value `<tag name={ term }>`,
and interpolations of a sequence of attributes `<tag {... term }/>`.
Character references are decoded in double-quoted values. {term}
    | An [HTML attribute](https://html.spec.whatwg.org/dev/syntax.html#attributes-2).
We support double-quoted attribute values `<tag name="val">`,
empty attributes `<tag name>`,
interpolations of one value `<tag name={ term }>`,
and interpolations of a sequence of attributes `<tag {... term }/>`.
Character references are decoded in double-quoted values. {...term}

Besides standard HTML features, the grammar above includes interpolations written with curly braces. These are holes in the syntax, filled in with a Lean term of the correct type (cf. string interpolation). They are supported in:

Content

  • Given an html : Html value, we can write html%{<tag>{html}</tag>}.

  • Given multiple values htmls : Array Html, or more generally any collection htmls' : ρ with a ForIn Id ρ Html instance, we can write html%{<tag>{...htmls}{...htmls'}</tag>}.

Attributes
Attribute values

Given val : String, we can write html%{<tag attr-name={val} />}.

HTML character references in text and in double-quoted attribute values are decoded to the Unicode characters they represent.

Character reference in HTML literal
ofArray #[text "<"] : Html#check html%{&lt;}
Live ↪

Whitespace in HTML content is governed by the following rules:

  • Whitespace that contains a newline (U+000A or U+000D), and is not surrounded by text on both sides, is removed.

  • Other consecutive whitespace is collapsed into a single space (U+0020).

Whitespace in HTML literal
ofArray #[element "ul" #[] (ofArray #[element "li" #[] (ofArray #[text "Item 1"]), element "li" #[] (ofArray #[text "Item 2"]), element "li" #[] (ofArray #[text "Item ", element "b" #[] (ofArray #[text "3"])])])] : Html#check html%{ <ul> <li>Item 1</li> <li>Item 2</li> <li>Item <b>3</b></li> </ul> }
Live ↪

26.2.2.1. Custom elaborators🔗

The HTML syntax is designed to support elaboration into custom types besides the Html type. It is implemented in Lean.Data.Html.Syntax as a collection of Parsers. The top-level parser is Syntax.content. No syntax category is declared.

Elaboration is facilitated by view functions that provide convenient descriptions of the parsed syntax. For instance, the Syntax.Content.view function describes a Syntax.Content node as a sequence of items. (Syntax.Content is an alias for TSyntax Syntax.contentKind.)

The html%{} literal elaborator in Lean.Data.Html.Elab is a useful example of how to use views.

🔗def
Lean.Html.Syntax.Content.view {m : Type → Type} [Monad m] [MonadError m]
  (c : Syntax.Content) : m (Array Syntax.ContentItemView)
Lean.Html.Syntax.Content.view
  {m : Type → Type} [Monad m]
  [MonadError m] (c : Syntax.Content) :
  m (Array Syntax.ContentItemView)

Returns the sequence of items in an HTML content node.

Runs of text interspersed with comments are merged into a single item. This is because their text must be processed together into a single output (see TextCommentsView.getText).

🔗inductive type
Lean.Html.Syntax.ContentItemView : Type
Lean.Html.Syntax.ContentItemView : Type

Constructors

Lean.Html.Syntax.ContentItemView.element
  (stx : Syntax.Element) : Syntax.ContentItemView
Lean.Html.Syntax.ContentItemView.textComments
  (stx : Syntax.TextCommentsView) : Syntax.ContentItemView
Lean.Html.Syntax.ContentItemView.interp (isMany : Bool)
  (stx : Syntax.Interp isMany) : Syntax.ContentItemView

Views implement details of whitespace handling and character reference decoding, simplifying elaborator implementations.

They operate at one level of depth: a view describes the current syntax node, but the arguments to its constructors are again ordinary Lean.TSyntax, as opposed to being themselves described by nested views. For instance, the argument to Syntax.ContentItemView.element is Syntax.Element (an alias for TSyntax Syntax.elementKind), not Syntax.ElementView. An elaborator based on views progressively invokes view functions whenever it needs to inspect more syntax.

26.2.2.2. Adherence to WhatWG Specification🔗

The HTML syntax is optimized for authoring HTML content within Lean, rather than parsing existing HTML documents. As such, is not guaranteed to comply with the WhatWG specification. That said, it tries to match the specification in most cases; known departures from the specification are documented on the relevant parser.