@[reducible, inline]

abbrev Lean.Xml.Parser.LeanChar : Type

Equations

• Lean.Xml.Parser.LeanChar = Char

def Lean.Xml.Parser.endl : Lean.Parsec 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 : Lean.Parsec α) : Lean.Parsec α

Equations

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

def Lean.Xml.Parser.Char : Lean.Parsec 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 : Lean.Parsec String

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

Equations

• Lean.Xml.Parser.S = (HOrElse.hOrElse (Lean.Parsec.pchar ' ') fun (x : Unit) => HOrElse.hOrElse Lean.Xml.Parser.endl fun (x : Unit) => Lean.Parsec.pchar '\t').many1Chars

def Lean.Xml.Parser.Eq : Lean.Parsec 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) => Lean.Parsec.skipChar '=') fun (x : Unit) => optional Lean.Xml.Parser.S

def Lean.Xml.Parser.NameStartChar : Lean.Parsec 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 : Lean.Parsec 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 : Lean.Parsec String

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

Equations

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

def Lean.Xml.Parser.VersionNum : Lean.Parsec Unit

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

Equations

• Lean.Xml.Parser.VersionNum = SeqLeft.seqLeft (Lean.Parsec.skipString "1.") fun (x : Unit) => Lean.Parsec.digit.many1

def Lean.Xml.Parser.VersionInfo : Lean.Parsec Unit

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

Equations

• Lean.Xml.Parser.VersionInfo = do SeqRight.seqRight Lean.Xml.Parser.S fun (x : Unit) => Lean.Parsec.skipString "version" Lean.Xml.Parser.Eq Lean.Xml.Parser.quote Lean.Xml.Parser.VersionNum

def Lean.Xml.Parser.EncName : Lean.Parsec 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 : Lean.Parsec String

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

Equations

• Lean.Xml.Parser.EncodingDecl = do SeqRight.seqRight Lean.Xml.Parser.S fun (x : Unit) => Lean.Parsec.skipString "encoding" Lean.Xml.Parser.Eq Lean.Xml.Parser.quote Lean.Xml.Parser.EncName

def Lean.Xml.Parser.SDDecl : Lean.Parsec 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 : Lean.Parsec 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 : Lean.Parsec 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 : Lean.Parsec 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 : Lean.Parsec 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 : Lean.Parsec 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 : Lean.Parsec 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 : Lean.Parsec 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 : Lean.Parsec 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 : Lean.Parsec 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 : Lean.Parsec 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 : Lean.Parsec Unit

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

partial def Lean.Xml.Parser.choice : Lean.Parsec Unit

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

partial def Lean.Xml.Parser.seq : Lean.Parsec Unit

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

def Lean.Xml.Parser.children : Lean.Parsec 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 : Lean.Parsec 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 : Lean.Parsec 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 : Lean.Parsec Unit

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

Equations

• Lean.Xml.Parser.StringType = Lean.Parsec.skipString "CDATA"

def Lean.Xml.Parser.TokenizedType : Lean.Parsec 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 : Lean.Parsec 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 : Lean.Parsec String

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

Equations

• Lean.Xml.Parser.Nmtoken = Lean.Xml.Parser.NameChar.many1Chars

def Lean.Xml.Parser.Enumeration : Lean.Parsec 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 : Lean.Parsec 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 : Lean.Parsec 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 x = match x with | "lt" => some '<' | "gt" => some '>' | "amp" => some '&' | "apos" => some ''' | "quot" => some '\"' | x => none

def Lean.Xml.Parser.EntityRef : Lean.Parsec (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 : Lean.Parsec 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 : Lean.Parsec (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 : Lean.Parsec 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 : Lean.Parsec 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 : Lean.Parsec 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 : Lean.Parsec 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 : Lean.Parsec Unit

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

Equations

• Lean.Xml.Parser.PEReference = SeqRight.seqRight (SeqRight.seqRight (Lean.Parsec.skipChar '%') fun (x : Unit) => Lean.Xml.Parser.Name) fun (x : Unit) => Lean.Parsec.skipChar ';'

def Lean.Xml.Parser.EntityValue : Lean.Parsec 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 : Lean.Parsec 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 : Lean.Parsec 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 : Lean.Parsec 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 : Lean.Parsec 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 : Lean.Parsec 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 : Lean.Parsec 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 : Lean.Parsec Unit

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

Equations

• Lean.Xml.Parser.PublicID = SeqLeft.seqLeft (SeqLeft.seqLeft (Lean.Parsec.skipString "PUBLIC") fun (x : Unit) => Lean.Xml.Parser.S) fun (x : Unit) => Lean.Xml.Parser.PubidLiteral

def Lean.Xml.Parser.NotationDecl : Lean.Parsec 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 : Lean.Parsec 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 : Lean.Parsec 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 : Lean.Parsec Unit

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

Equations

• Lean.Xml.Parser.intSubset = SeqRight.seqRight (HOrElse.hOrElse Lean.Xml.Parser.markupDecl fun (x : Unit) => Lean.Xml.Parser.DeclSep).many fun (x : Unit) => pure ()

def Lean.Xml.Parser.doctypedecl : Lean.Parsec 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 : Lean.Parsec 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 : Lean.Parsec (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 : Lean.Parsec (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) : Lean.Parsec Lean.Xml.Element

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

Equations

• Lean.Xml.Parser.EmptyElemTag elem = SeqRight.seqRight (Lean.Parsec.skipString "/>") fun (x : Unit) => pure (elem #[])

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

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

Equations

• Lean.Xml.Parser.STag elem = SeqRight.seqRight (Lean.Parsec.skipChar '>') fun (x : Unit) => pure elem

def Lean.Xml.Parser.ETag : Lean.Parsec 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 : Lean.Parsec Unit

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

Equations

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

def Lean.Xml.Parser.CDEnd : Lean.Parsec Unit

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

Equations

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

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

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

Equations

• Lean.Xml.Parser.CData = (SeqRight.seqRight (Lean.Parsec.skipString "]]>").notFollowedBy fun (x : Unit) => Lean.Parsec.anyChar).manyChars

def Lean.Xml.Parser.CDSect : Lean.Parsec 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 : Lean.Parsec String

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

Equations

• Lean.Xml.Parser.CharData = SeqRight.seqRight (Lean.Parsec.skipString "]]>").notFollowedBy fun (x : Unit) => (Lean.Parsec.satisfy fun (c : Char) => decide (c ≠ '<' ∧ c ≠ '&')).manyChars

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

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

partial def Lean.Xml.Parser.element : Lean.Parsec Lean.Xml.Element

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

def Lean.Xml.Parser.document : Lean.Parsec 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

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