@[reducible, inline]

abbrev Lean.Xml.Parser.LeanChar : Type

Equations

• Lean.Xml.Parser.LeanChar = Char

def Lean.Xml.Parser.endl : Std.Internal.Parsec.String.Parser Lean.Xml.Parser.LeanChar

consume a newline character sequence pretending, that we read '\n'. As per spec: https://www.w3.org/TR/xml/#sec-line-ends

Equations

• Lean.Xml.Parser.endl = (Std.Internal.Parsec.String.skipString "\x0d\n" <|> Std.Internal.Parsec.String.skipChar '\x0d' <|> Std.Internal.Parsec.String.skipChar '\n') *> pure '\n'

def Lean.Xml.Parser.quote {α : Type} (p : Std.Internal.Parsec.String.Parser α) : Std.Internal.Parsec.String.Parser α

Equations

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

def Lean.Xml.Parser.Char : Std.Internal.Parsec.String.Parser Lean.Xml.Parser.LeanChar

https://www.w3.org/TR/xml/#NT-Char

Equations

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

def Lean.Xml.Parser.S : Std.Internal.Parsec.String.Parser String

https://www.w3.org/TR/xml/#NT-S

Equations

• Lean.Xml.Parser.S = Std.Internal.Parsec.many1Chars (Std.Internal.Parsec.String.pchar ' ' <|> Lean.Xml.Parser.endl <|> Std.Internal.Parsec.String.pchar '\t')

def Lean.Xml.Parser.Eq : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-Eq

Equations

• Lean.Xml.Parser.Eq = optional Lean.Xml.Parser.S *> Std.Internal.Parsec.String.skipChar '=' <* optional Lean.Xml.Parser.S

def Lean.Xml.Parser.NameStartChar : Std.Internal.Parsec.String.Parser Lean.Xml.Parser.LeanChar

https://www.w3.org/TR/xml/#NT-NameStartChar

Equations

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

def Lean.Xml.Parser.NameChar : Std.Internal.Parsec.String.Parser Lean.Xml.Parser.LeanChar

https://www.w3.org/TR/xml/#NT-NameChar

Equations

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

def Lean.Xml.Parser.Name : Std.Internal.Parsec.String.Parser String

https://www.w3.org/TR/xml/#NT-Name

Equations

• Lean.Xml.Parser.Name = do let x ← Lean.Xml.Parser.NameStartChar Std.Internal.Parsec.manyCharsCore Lean.Xml.Parser.NameChar (Char.toString x)

def Lean.Xml.Parser.VersionNum : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-VersionNum

Equations

• Lean.Xml.Parser.VersionNum = Std.Internal.Parsec.String.skipString "1." <* Std.Internal.Parsec.many1 Std.Internal.Parsec.String.digit

def Lean.Xml.Parser.VersionInfo : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-VersionInfo

Equations

• Lean.Xml.Parser.VersionInfo = do Lean.Xml.Parser.S *> Std.Internal.Parsec.String.skipString "version" Lean.Xml.Parser.Eq Lean.Xml.Parser.quote Lean.Xml.Parser.VersionNum

def Lean.Xml.Parser.EncName : Std.Internal.Parsec.String.Parser String

https://www.w3.org/TR/xml/#NT-EncName

Equations

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

def Lean.Xml.Parser.EncodingDecl : Std.Internal.Parsec.String.Parser String

https://www.w3.org/TR/xml/#NT-EncodingDecl

Equations

• Lean.Xml.Parser.EncodingDecl = do Lean.Xml.Parser.S *> Std.Internal.Parsec.String.skipString "encoding" Lean.Xml.Parser.Eq Lean.Xml.Parser.quote Lean.Xml.Parser.EncName

def Lean.Xml.Parser.SDDecl : Std.Internal.Parsec.String.Parser String

https://www.w3.org/TR/xml/#NT-SDDecl

Equations

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

def Lean.Xml.Parser.XMLdecl : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-XMLDecl

Equations

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

def Lean.Xml.Parser.Comment : Std.Internal.Parsec.String.Parser String

https://www.w3.org/TR/xml/#NT-Comment

Equations

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

def Lean.Xml.Parser.PITarget : Std.Internal.Parsec.String.Parser String

https://www.w3.org/TR/xml/#NT-PITarget

Equations

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

def Lean.Xml.Parser.PI : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-PI

Equations

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

def Lean.Xml.Parser.Misc : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-Misc

Equations

• Lean.Xml.Parser.Misc = (Lean.Xml.Parser.Comment *> pure () <|> Lean.Xml.Parser.PI <|> Lean.Xml.Parser.S *> pure ())

def Lean.Xml.Parser.SystemLiteral : Std.Internal.Parsec.String.Parser String

https://www.w3.org/TR/xml/#NT-SystemLiteral

Equations

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

def Lean.Xml.Parser.PubidChar : Std.Internal.Parsec.String.Parser Lean.Xml.Parser.LeanChar

https://www.w3.org/TR/xml/#NT-PubidChar

Equations

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

def Lean.Xml.Parser.PubidLiteral : Std.Internal.Parsec.String.Parser String

https://www.w3.org/TR/xml/#NT-PubidLiteral

Equations

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

def Lean.Xml.Parser.ExternalID : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-ExternalID

Equations

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

def Lean.Xml.Parser.Mixed : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-Mixed

Equations

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

partial def Lean.Xml.Parser.cp : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-cp

partial def Lean.Xml.Parser.choice : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-choice

partial def Lean.Xml.Parser.seq : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-seq

def Lean.Xml.Parser.children : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-children

Equations

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

def Lean.Xml.Parser.contentspec : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-contentspec

Equations

• Lean.Xml.Parser.contentspec = (Std.Internal.Parsec.String.skipString "EMPTY" <|> Std.Internal.Parsec.String.skipString "ANY" <|> Lean.Xml.Parser.Mixed <|> Lean.Xml.Parser.children)

def Lean.Xml.Parser.elementDecl : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-elementdecl

Equations

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

def Lean.Xml.Parser.StringType : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-StringType

Equations

• Lean.Xml.Parser.StringType = Std.Internal.Parsec.String.skipString "CDATA"

def Lean.Xml.Parser.TokenizedType : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-TokenizedType

Equations

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

def Lean.Xml.Parser.NotationType : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-NotationType

Equations

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

def Lean.Xml.Parser.Nmtoken : Std.Internal.Parsec.String.Parser String

https://www.w3.org/TR/xml/#NT-Nmtoken

Equations

• Lean.Xml.Parser.Nmtoken = Std.Internal.Parsec.many1Chars Lean.Xml.Parser.NameChar

def Lean.Xml.Parser.Enumeration : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-Enumeration

Equations

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

def Lean.Xml.Parser.EnumeratedType : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-EnumeratedType

Equations

• Lean.Xml.Parser.EnumeratedType = (Lean.Xml.Parser.NotationType <|> Lean.Xml.Parser.Enumeration)

def Lean.Xml.Parser.AttType : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-AttType

Equations

• Lean.Xml.Parser.AttType = (Lean.Xml.Parser.StringType <|> Lean.Xml.Parser.TokenizedType <|> Lean.Xml.Parser.EnumeratedType)

def Lean.Xml.Parser.predefinedEntityToChar : String → Option Lean.Xml.Parser.LeanChar

Equations

• Lean.Xml.Parser.predefinedEntityToChar "lt" = some '<'
• Lean.Xml.Parser.predefinedEntityToChar "gt" = some '>'
• Lean.Xml.Parser.predefinedEntityToChar "amp" = some '&'
• Lean.Xml.Parser.predefinedEntityToChar "apos" = some '''
• Lean.Xml.Parser.predefinedEntityToChar "quot" = some '\"'
• Lean.Xml.Parser.predefinedEntityToChar x✝ = none

def Lean.Xml.Parser.EntityRef : Std.Internal.Parsec.String.Parser (Option Lean.Xml.Parser.LeanChar)

https://www.w3.org/TR/xml/#NT-EntityRef

Equations

• Lean.Xml.Parser.EntityRef = (Std.Internal.Parsec.String.skipChar '&' *> Lean.Xml.Parser.predefinedEntityToChar <$> Lean.Xml.Parser.Name <* Std.Internal.Parsec.String.skipChar ';').attempt

@[inline]

def Lean.Xml.Parser.hexDigitToNat (c : Lean.Xml.Parser.LeanChar) : Nat

Equations

• Lean.Xml.Parser.hexDigitToNat c = if '0' ≤ c ∧ c ≤ '9' then Char.toNat c - '0'.toNat else if 'a' ≤ c ∧ c ≤ 'f' then Char.toNat c - 'a'.toNat + 10 else Char.toNat c - 'A'.toNat + 10

def Lean.Xml.Parser.digitsToNat (base : Nat) (digits : Array Nat) : Nat

Equations

• Lean.Xml.Parser.digitsToNat base digits = Array.foldl (fun (r d : Nat) => r * base + d) 0 digits

def Lean.Xml.Parser.CharRef : Std.Internal.Parsec.String.Parser Lean.Xml.Parser.LeanChar

https://www.w3.org/TR/xml/#NT-CharRef

Equations

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

def Lean.Xml.Parser.Reference : Std.Internal.Parsec.String.Parser (Option Lean.Xml.Parser.LeanChar)

https://www.w3.org/TR/xml/#NT-Reference

Equations

• Lean.Xml.Parser.Reference = (Lean.Xml.Parser.EntityRef <|> some <$> Lean.Xml.Parser.CharRef)

def Lean.Xml.Parser.AttValue : Std.Internal.Parsec.String.Parser String

https://www.w3.org/TR/xml/#NT-AttValue

Equations

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

def Lean.Xml.Parser.DefaultDecl : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-DefaultDecl

Equations

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

def Lean.Xml.Parser.AttDef : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-AttDef

Equations

• Lean.Xml.Parser.AttDef = Lean.Xml.Parser.S *> Lean.Xml.Parser.Name *> Lean.Xml.Parser.S *> Lean.Xml.Parser.AttType *> Lean.Xml.Parser.S *> Lean.Xml.Parser.DefaultDecl

def Lean.Xml.Parser.AttlistDecl : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-AttlistDecl

Equations

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

def Lean.Xml.Parser.PEReference : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-PEReference

Equations

• Lean.Xml.Parser.PEReference = Std.Internal.Parsec.String.skipChar '%' *> Lean.Xml.Parser.Name *> Std.Internal.Parsec.String.skipChar ';'

def Lean.Xml.Parser.EntityValue : Std.Internal.Parsec.String.Parser String

https://www.w3.org/TR/xml/#NT-EntityValue

Equations

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

def Lean.Xml.Parser.NDataDecl : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-NDataDecl

Equations

• Lean.Xml.Parser.NDataDecl = Lean.Xml.Parser.S *> Std.Internal.Parsec.String.skipString "NDATA" <* Lean.Xml.Parser.S <* Lean.Xml.Parser.Name

def Lean.Xml.Parser.EntityDef : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-EntityDef

Equations

• Lean.Xml.Parser.EntityDef = (Lean.Xml.Parser.EntityValue *> pure () <|> Lean.Xml.Parser.ExternalID <* optional Lean.Xml.Parser.NDataDecl)

def Lean.Xml.Parser.GEDecl : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-GEDecl

Equations

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

def Lean.Xml.Parser.PEDef : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-PEDef

Equations

• Lean.Xml.Parser.PEDef = (Lean.Xml.Parser.EntityValue *> pure () <|> Lean.Xml.Parser.ExternalID)

def Lean.Xml.Parser.PEDecl : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-PEDecl

Equations

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

def Lean.Xml.Parser.EntityDecl : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-EntityDecl

Equations

• Lean.Xml.Parser.EntityDecl = (Lean.Xml.Parser.GEDecl <|> Lean.Xml.Parser.PEDecl)

def Lean.Xml.Parser.PublicID : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-PublicID

Equations

• Lean.Xml.Parser.PublicID = Std.Internal.Parsec.String.skipString "PUBLIC" <* Lean.Xml.Parser.S <* Lean.Xml.Parser.PubidLiteral

def Lean.Xml.Parser.NotationDecl : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-NotationDecl

Equations

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

def Lean.Xml.Parser.markupDecl : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-markupdecl

Equations

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

def Lean.Xml.Parser.DeclSep : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-DeclSep

Equations

• Lean.Xml.Parser.DeclSep = (Lean.Xml.Parser.PEReference <|> Lean.Xml.Parser.S *> pure ())

def Lean.Xml.Parser.intSubset : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-intSubset

Equations

• Lean.Xml.Parser.intSubset = Std.Internal.Parsec.many (Lean.Xml.Parser.markupDecl <|> Lean.Xml.Parser.DeclSep) *> pure ()

def Lean.Xml.Parser.doctypedecl : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-doctypedecl

Equations

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

def Lean.Xml.Parser.prolog : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-prolog

Equations

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

def Lean.Xml.Parser.Attribute : Std.Internal.Parsec.String.Parser (String × String)

https://www.w3.org/TR/xml/#NT-Attribute

Equations

• Lean.Xml.Parser.Attribute = do let name ← Lean.Xml.Parser.Name Lean.Xml.Parser.Eq let value ← Lean.Xml.Parser.AttValue pure (name, value)

def Lean.Xml.Parser.elementPrefix : Std.Internal.Parsec.String.Parser (Array Lean.Xml.Content → Lean.Xml.Element)

Equations

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

def Lean.Xml.Parser.EmptyElemTag (elem : Array Lean.Xml.Content → Lean.Xml.Element) : Std.Internal.Parsec.String.Parser Lean.Xml.Element

https://www.w3.org/TR/xml/#NT-EmptyElemTag

Equations

• Lean.Xml.Parser.EmptyElemTag elem = Std.Internal.Parsec.String.skipString "/>" *> pure (elem #[])

def Lean.Xml.Parser.STag (elem : Array Lean.Xml.Content → Lean.Xml.Element) : Std.Internal.Parsec.String.Parser (Array Lean.Xml.Content → Lean.Xml.Element)

https://www.w3.org/TR/xml/#NT-STag

Equations

• Lean.Xml.Parser.STag elem = Std.Internal.Parsec.String.skipChar '>' *> pure elem

def Lean.Xml.Parser.ETag : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-ETag

Equations

• Lean.Xml.Parser.ETag = Std.Internal.Parsec.String.skipString "</" *> Lean.Xml.Parser.Name *> optional Lean.Xml.Parser.S *> Std.Internal.Parsec.String.skipChar '>'

def Lean.Xml.Parser.CDStart : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-CDStart

Equations

• Lean.Xml.Parser.CDStart = Std.Internal.Parsec.String.skipString "<![CDATA["

def Lean.Xml.Parser.CDEnd : Std.Internal.Parsec.String.Parser Unit

https://www.w3.org/TR/xml/#NT-CDEnd

Equations

• Lean.Xml.Parser.CDEnd = Std.Internal.Parsec.String.skipString "]]>"

def Lean.Xml.Parser.CData : Std.Internal.Parsec.String.Parser String

https://www.w3.org/TR/xml/#NT-CData

Equations

• Lean.Xml.Parser.CData = (Std.Internal.Parsec.notFollowedBy (Std.Internal.Parsec.String.skipString "]]>") *> Std.Internal.Parsec.any).manyChars

def Lean.Xml.Parser.CDSect : Std.Internal.Parsec.String.Parser String

https://www.w3.org/TR/xml/#NT-CDSect

Equations

• Lean.Xml.Parser.CDSect = Lean.Xml.Parser.CDStart *> Lean.Xml.Parser.CData <* Lean.Xml.Parser.CDEnd

def Lean.Xml.Parser.CharData : Std.Internal.Parsec.String.Parser String

https://www.w3.org/TR/xml/#NT-CharData

Equations

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

partial def Lean.Xml.Parser.content : Std.Internal.Parsec.String.Parser (Array Lean.Xml.Content)

https://www.w3.org/TR/xml/#NT-content

partial def Lean.Xml.Parser.element : Std.Internal.Parsec.String.Parser Lean.Xml.Element

https://www.w3.org/TR/xml/#NT-element

def Lean.Xml.Parser.document : Std.Internal.Parsec.String.Parser Lean.Xml.Element

https://www.w3.org/TR/xml/#NT-document

Equations

• Lean.Xml.Parser.document = Lean.Xml.Parser.prolog *> Lean.Xml.Parser.element <* Std.Internal.Parsec.many Lean.Xml.Parser.Misc <* Std.Internal.Parsec.eof

def Lean.Xml.parse (s : String) : Except String Lean.Xml.Element

Equations

• Lean.Xml.parse s = Lean.Xml.Parser.document.run s