def Lean.Html.Syntax.Element.checkNamesMatch (stx : Element) : CoreM Unit

Throws an informative error when the start and end tag names do not match (up to casing).

Equations

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

def Lean.Html.Syntax.Element.checkNoVoidChildren (stx : Element) : CoreM Unit

Throws an informative error when the element should be void, yet has children.

Equations

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