@[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

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

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

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

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

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

Equations

• Lean.Xml.Parser.Eq = SeqLeft.seqLeft (SeqRight.seqRight (optional Lean.Xml.Parser.S) fun (x : Unit) => Std.Internal.Parsec.String.skipChar '=') fun (x : Unit) => 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 = SeqLeft.seqLeft (Std.Internal.Parsec.String.skipString "1.") fun (x : Unit) => 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

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

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

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

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

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

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

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

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 = HOrElse.hOrElse Lean.Xml.Parser.NotationType fun (x : Unit) => 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 = HOrElse.hOrElse Lean.Xml.Parser.StringType fun (x : Unit) => HOrElse.hOrElse Lean.Xml.Parser.TokenizedType fun (x : Unit) => 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

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

@[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 = HOrElse.hOrElse Lean.Xml.Parser.EntityRef fun (x : Unit) => 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

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

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

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

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

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

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

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

Equations

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

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 = HOrElse.hOrElse (SeqRight.seqRight Lean.Xml.Parser.EntityValue fun (x : Unit) => pure ()) fun (x : Unit) => 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 = HOrElse.hOrElse Lean.Xml.Parser.GEDecl fun (x : Unit) => 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 = SeqLeft.seqLeft (SeqLeft.seqLeft (Std.Internal.Parsec.String.skipString "PUBLIC") fun (x : Unit) => Lean.Xml.Parser.S) fun (x : Unit) => 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 = HOrElse.hOrElse Lean.Xml.Parser.PEReference fun (x : Unit) => SeqRight.seqRight Lean.Xml.Parser.S fun (x : Unit) => 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 = SeqRight.seqRight (Std.Internal.Parsec.many (HOrElse.hOrElse Lean.Xml.Parser.markupDecl fun (x : Unit) => Lean.Xml.Parser.DeclSep)) fun (x : Unit) => 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 = SeqRight.seqRight (Std.Internal.Parsec.String.skipString "/>") fun (x : Unit) => 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 = SeqRight.seqRight (Std.Internal.Parsec.String.skipChar '>') fun (x : Unit) => pure elem

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

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

Equations

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

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 = (SeqRight.seqRight (Std.Internal.Parsec.notFollowedBy (Std.Internal.Parsec.String.skipString "]]>")) fun (x : Unit) => 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 = SeqLeft.seqLeft (SeqRight.seqRight Lean.Xml.Parser.CDStart fun (x : Unit) => Lean.Xml.Parser.CData) fun (x : Unit) => 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

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

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

Equations

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