Lean.Data.Xml.Parser

source

@[inline]

abbrev Lean.Xml.Parser.LeanChar:

Type

Equations

Lean.Xml.Parser.LeanChar = Char

source

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.

source

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

Lean.Parsec α

Equations

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

source

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.

source

def Lean.Xml.Parser.S:

Lean.Parsec String

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

Equations

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

source

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 => Lean.Parsec.skipChar (Char.ofNat 61)) fun x => optional Lean.Xml.Parser.S

source

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.

source

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.

source

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.Parsec.manyCharsCore Lean.Xml.Parser.NameChar (Char.toString x)

source

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 => Lean.Parsec.many1 Lean.Parsec.digit

source

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 => Lean.Parsec.skipString "version" Lean.Xml.Parser.Eq Lean.Xml.Parser.quote Lean.Xml.Parser.VersionNum

source

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.

source

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 => Lean.Parsec.skipString "encoding" Lean.Xml.Parser.Eq Lean.Xml.Parser.quote Lean.Xml.Parser.EncName

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

partial def Lean.Xml.Parser.cp:

Lean.Parsec Unit

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

source

partial def Lean.Xml.Parser.choice:

Lean.Parsec Unit

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

source

partial def Lean.Xml.Parser.seq:

Lean.Parsec Unit

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

source

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.

source

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.

source

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.

source

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"

source

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.

source

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.

source

def Lean.Xml.Parser.Nmtoken:

Lean.Parsec String

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

Equations

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

source

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.

source

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 => Lean.Xml.Parser.Enumeration

source

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 => HOrElse.hOrElse Lean.Xml.Parser.TokenizedType fun x => Lean.Xml.Parser.EnumeratedType

source

def Lean.Xml.Parser.predefinedEntityToChar:

String → Option Lean.Xml.Parser.LeanChar

Equations

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

source

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.

source

@[inline]

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

Nat

Equations

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

source

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

Nat

Equations

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

source

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.

source

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 => some <$> Lean.Xml.Parser.CharRef

source

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.

source

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.

source

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.

source

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.

source

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 (Char.ofNat 37)) fun x => Lean.Xml.Parser.Name) fun x => Lean.Parsec.skipChar (Char.ofNat 59)

source

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.

source

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.

source

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.

source

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.

source

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 => pure ()) fun x => Lean.Xml.Parser.ExternalID

source

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.

source

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 => Lean.Xml.Parser.PEDecl

source

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 => Lean.Xml.Parser.S) fun x => Lean.Xml.Parser.PubidLiteral

source

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.

source

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.

source

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 => SeqRight.seqRight Lean.Xml.Parser.S fun x => pure ()

source

def Lean.Xml.Parser.intSubset:

Lean.Parsec Unit

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

Equations

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

source

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.

source

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.

source

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)

source

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.

source

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 => pure (elem #[])

source

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 (Char.ofNat 62)) fun x => pure elem

source

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.

source

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

source

def Lean.Xml.Parser.CDEnd:

Lean.Parsec Unit

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

Equations

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

source

def Lean.Xml.Parser.CData:

Lean.Parsec String

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

Equations

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

source

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 => Lean.Xml.Parser.CData) fun x => Lean.Xml.Parser.CDEnd

source

def Lean.Xml.Parser.CharData:

Lean.Parsec String

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

Equations

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

source

partial def Lean.Xml.Parser.content:

Lean.Parsec (Array Lean.Xml.Content)

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

source

partial def Lean.Xml.Parser.element:

Lean.Parsec Lean.Xml.Element

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

source

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.

source

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

Except String Lean.Xml.Element

Equations

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