Documentation

Lean.Data.Xml.Basic

noncomputable def Lean.Xml.Attributes :

Type

Equations

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

instance Lean.Xml.instToStringAttributes :

ToString Lean.Xml.Attributes

Equations

Lean.Xml.instToStringAttributes = { toString := fun as => Std.RBMap.fold (fun s n v => s ++ (toString " " ++ toString n ++ toString "=\"" ++ toString v ++ toString "\"")) "" as }

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 }