Code points

def Lean.Html.isControl (c : Char) : Bool

Whether c is a control code point.

Equations

• Lean.Html.isControl c = (decide (c.toNat ≤ 31) || decide (c.toNat ≥ 127) && decide (c.toNat ≤ 159))

def Lean.Html.isAsciiWhitespace (c : Char) : Bool

Whether c is ASCII whitespace. Differs from Char.isWhitespace by also including FF U+000C.

Equations

• Lean.Html.isAsciiWhitespace c = decide (c.toNat ∈ [9, 10, 12, 13, 32])

def Lean.Html.isNonCharacter (c : Char) : Bool

Whether c is a noncharacter.

Equations

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

Tag names

def Lean.Html.isVoidElement (tagName : String) : Bool

Whether tagName (compared case-insensitively) names a void element.

Void elements are those that cannot have any child nodes. These only have a start tag; end tags must not be specified. See https://html.spec.whatwg.org/dev/syntax.html#void-elements.

Equations

• Lean.Html.isVoidElement tagName = Lean.Html.voidElements✝.binSearchContains tagName.toLower fun (x1 x2 : String) => decide (x1 < x2)