def Lean.Html.namedCharacterReference? (ref : String) : Option String

Looks up the string denoted by the body ref of an HTML named character reference &ref;. Returns none when &ref; is not listed in the HTML standard.

Equations

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

def Lean.Html.characterReference? (ref : String) : Option String

Looks up the string denoted by the body ref of an HTML character reference &ref;. Returns none when &ref; is not valid per the HTML standard.

Named references (such as &) must be listed in the HTML standard. Numeric references in decimal ({) or hexadecimal ({) notation must denote a Unicode scalar value that is not U+0000, U+000D, a noncharacter, or a control other than ASCII whitespace.

Equations

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