Documentation

Lean.Data.Html.Elab

source
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).

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

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

    Instances For