Documentation
Lean
.
Data
.
Xml
.
Basic
Search
return to top
source
Imports
Lean.Data.RBMap
Init.Data.ToString.Macro
Imported by
Lean
.
Xml
.
Attributes
Lean
.
Xml
.
instToStringAttributes
Lean
.
Xml
.
Element
Lean
.
Xml
.
Content
Lean
.
Xml
.
instInhabitedContent
Lean
.
Xml
.
instToStringElement
Lean
.
Xml
.
instToStringContent
source
def
Lean
.
Xml
.
Attributes
:
Type
Equations
Instances For
source
instance
Lean
.
Xml
.
instToStringAttributes
:
ToString
Attributes
Equations
source
inductive
Lean
.
Xml
.
Element
:
Type
Element
(
name
:
String
)
(
attributes
:
Attributes
)
(
content
:
Array
Content
)
:
Xml.Element
Instances For
source
inductive
Lean
.
Xml
.
Content
:
Type
Element
(
element
:
Xml.Element
)
:
Content
Comment
(
comment
:
String
)
:
Content
Character
(
content
:
String
)
:
Content
Instances For
source
instance
Lean
.
Xml
.
instInhabitedContent
:
Inhabited
Content
Equations
source
instance
Lean
.
Xml
.
instToStringElement
:
ToString
Element
Equations
source
instance
Lean
.
Xml
.
instToStringContent
:
ToString
Content
Equations