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.