Documentation

Lean.Data.Xml.Basic

def Lean.Xml.Attributes:

Type

Equations

Lean.Xml.Attributes = Std.RBMap String String compare

instance Lean.Xml.instToStringAttributes:

ToString Lean.Xml.Attributes

Equations

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

inductive Lean.Xml.Element:

Type

Element: String → Lean.Xml.Attributes → Array Lean.Xml.Content → Lean.Xml.Element

inductive Lean.Xml.Content:

Type

Element: Lean.Xml.Element → Lean.Xml.Content
Comment: String → Lean.Xml.Content
Character: String → Lean.Xml.Content

instance Lean.Xml.instInhabitedContent:

Inhabited Lean.Xml.Content

Equations

Lean.Xml.instInhabitedContent = { default := Lean.Xml.Content.Comment default }

instance Lean.Xml.instToStringElement:

ToString Lean.Xml.Element

Equations

Lean.Xml.instToStringElement = { toString := Lean.Xml.eToString }

instance Lean.Xml.instToStringContent:

ToString Lean.Xml.Content

Equations

Lean.Xml.instToStringContent = { toString := Lean.Xml.cToString }