Documentation

Lean.Data.Xml.Parser

source
@[reducible, inline]
abbrev Lean.Xml.Parser.LeanChar :
Type
Equations
    Instances For
      source
      def Lean.Xml.Parser.endl :
      Std.Internal.Parsec.String.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
        Instances For
          source
          def Lean.Xml.Parser.quote {α : Type} (p : Std.Internal.Parsec.String.Parser α) :
          Std.Internal.Parsec.String.Parser α
          Equations
            Instances For
              source
              def Lean.Xml.Parser.Char :
              Std.Internal.Parsec.String.Parser LeanChar

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

              Equations
                Instances For
                  source
                  def Lean.Xml.Parser.S :
                  Std.Internal.Parsec.String.Parser String

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

                  Equations
                    Instances For
                      source
                      def Lean.Xml.Parser.Eq :
                      Std.Internal.Parsec.String.Parser Unit

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

                      Equations
                        Instances For
                          source
                          def Lean.Xml.Parser.NameStartChar :
                          Std.Internal.Parsec.String.Parser LeanChar

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

                          Equations
                            Instances For
                              source
                              def Lean.Xml.Parser.NameChar :
                              Std.Internal.Parsec.String.Parser LeanChar

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

                              Equations
                                Instances For
                                  source
                                  def Lean.Xml.Parser.Name :
                                  Std.Internal.Parsec.String.Parser String

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

                                  Equations
                                    Instances For
                                      source
                                      def Lean.Xml.Parser.VersionNum :
                                      Std.Internal.Parsec.String.Parser Unit

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

                                      Equations
                                        Instances For
                                          source
                                          def Lean.Xml.Parser.VersionInfo :
                                          Std.Internal.Parsec.String.Parser Unit

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

                                          Equations
                                            Instances For
                                              source
                                              def Lean.Xml.Parser.EncName :
                                              Std.Internal.Parsec.String.Parser String

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

                                              Equations
                                                Instances For
                                                  source
                                                  def Lean.Xml.Parser.EncodingDecl :
                                                  Std.Internal.Parsec.String.Parser String

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

                                                  Equations
                                                    Instances For
                                                      source
                                                      def Lean.Xml.Parser.SDDecl :
                                                      Std.Internal.Parsec.String.Parser String

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

                                                      Equations
                                                        Instances For
                                                          source
                                                          def Lean.Xml.Parser.XMLdecl :
                                                          Std.Internal.Parsec.String.Parser Unit

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

                                                          Equations
                                                            Instances For
                                                              source
                                                              def Lean.Xml.Parser.Comment :
                                                              Std.Internal.Parsec.String.Parser String

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

                                                              Equations
                                                                Instances For
                                                                  source
                                                                  def Lean.Xml.Parser.PITarget :
                                                                  Std.Internal.Parsec.String.Parser String

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

                                                                  Equations
                                                                    Instances For
                                                                      source
                                                                      def Lean.Xml.Parser.PI :
                                                                      Std.Internal.Parsec.String.Parser Unit

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

                                                                      Equations
                                                                        Instances For
                                                                          source
                                                                          def Lean.Xml.Parser.Misc :
                                                                          Std.Internal.Parsec.String.Parser Unit

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

                                                                          Equations
                                                                            Instances For
                                                                              source
                                                                              def Lean.Xml.Parser.SystemLiteral :
                                                                              Std.Internal.Parsec.String.Parser String

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

                                                                              Equations
                                                                                Instances For
                                                                                  source
                                                                                  def Lean.Xml.Parser.PubidChar :
                                                                                  Std.Internal.Parsec.String.Parser LeanChar

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

                                                                                  Equations
                                                                                    Instances For
                                                                                      source
                                                                                      def Lean.Xml.Parser.PubidLiteral :
                                                                                      Std.Internal.Parsec.String.Parser String

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

                                                                                      Equations
                                                                                        Instances For
                                                                                          source
                                                                                          def Lean.Xml.Parser.ExternalID :
                                                                                          Std.Internal.Parsec.String.Parser Unit

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

                                                                                          Equations
                                                                                            Instances For
                                                                                              source
                                                                                              def Lean.Xml.Parser.Mixed :
                                                                                              Std.Internal.Parsec.String.Parser Unit

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

                                                                                              Equations
                                                                                                Instances For
                                                                                                  source
                                                                                                  partial def Lean.Xml.Parser.cp :
                                                                                                  Std.Internal.Parsec.String.Parser Unit

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

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

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

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

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

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

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

                                                                                                  Equations
                                                                                                    Instances For
                                                                                                      source
                                                                                                      def Lean.Xml.Parser.contentspec :
                                                                                                      Std.Internal.Parsec.String.Parser Unit

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

                                                                                                      Equations
                                                                                                        Instances For
                                                                                                          source
                                                                                                          def Lean.Xml.Parser.elementDecl :
                                                                                                          Std.Internal.Parsec.String.Parser Unit

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

                                                                                                          Equations
                                                                                                            Instances For
                                                                                                              source
                                                                                                              def Lean.Xml.Parser.StringType :
                                                                                                              Std.Internal.Parsec.String.Parser Unit

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

                                                                                                              Equations
                                                                                                                Instances For
                                                                                                                  source
                                                                                                                  def Lean.Xml.Parser.TokenizedType :
                                                                                                                  Std.Internal.Parsec.String.Parser Unit

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

                                                                                                                  Equations
                                                                                                                    Instances For
                                                                                                                      source
                                                                                                                      def Lean.Xml.Parser.NotationType :
                                                                                                                      Std.Internal.Parsec.String.Parser Unit

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

                                                                                                                      Equations
                                                                                                                        Instances For
                                                                                                                          source
                                                                                                                          def Lean.Xml.Parser.Nmtoken :
                                                                                                                          Std.Internal.Parsec.String.Parser String

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

                                                                                                                          Equations
                                                                                                                            Instances For
                                                                                                                              source
                                                                                                                              def Lean.Xml.Parser.Enumeration :
                                                                                                                              Std.Internal.Parsec.String.Parser Unit

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

                                                                                                                              Equations
                                                                                                                                Instances For
                                                                                                                                  source
                                                                                                                                  def Lean.Xml.Parser.EnumeratedType :
                                                                                                                                  Std.Internal.Parsec.String.Parser Unit

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

                                                                                                                                  Equations
                                                                                                                                    Instances For
                                                                                                                                      source
                                                                                                                                      def Lean.Xml.Parser.AttType :
                                                                                                                                      Std.Internal.Parsec.String.Parser Unit

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

                                                                                                                                      Equations
                                                                                                                                        Instances For
                                                                                                                                          source
                                                                                                                                          def Lean.Xml.Parser.predefinedEntityToChar :
                                                                                                                                          String → Option LeanChar
                                                                                                                                          Equations
                                                                                                                                            Instances For
                                                                                                                                              source
                                                                                                                                              def Lean.Xml.Parser.EntityRef :
                                                                                                                                              Std.Internal.Parsec.String.Parser (Option LeanChar)

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

                                                                                                                                              Equations
                                                                                                                                                Instances For
                                                                                                                                                  source
                                                                                                                                                  @[inline]
                                                                                                                                                  def Lean.Xml.Parser.hexDigitToNat (c : LeanChar) :
                                                                                                                                                  Nat
                                                                                                                                                  Equations
                                                                                                                                                    Instances For
                                                                                                                                                      source
                                                                                                                                                      def Lean.Xml.Parser.digitsToNat (base : Nat) (digits : Array Nat) :
                                                                                                                                                      Nat
                                                                                                                                                      Equations
                                                                                                                                                        Instances For
                                                                                                                                                          source
                                                                                                                                                          def Lean.Xml.Parser.CharRef :
                                                                                                                                                          Std.Internal.Parsec.String.Parser LeanChar

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

                                                                                                                                                          Equations
                                                                                                                                                            Instances For
                                                                                                                                                              source
                                                                                                                                                              def Lean.Xml.Parser.Reference :
                                                                                                                                                              Std.Internal.Parsec.String.Parser (Option LeanChar)

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

                                                                                                                                                              Equations
                                                                                                                                                                Instances For
                                                                                                                                                                  source
                                                                                                                                                                  def Lean.Xml.Parser.AttValue :
                                                                                                                                                                  Std.Internal.Parsec.String.Parser String

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

                                                                                                                                                                  Equations
                                                                                                                                                                    Instances For
                                                                                                                                                                      source
                                                                                                                                                                      def Lean.Xml.Parser.DefaultDecl :
                                                                                                                                                                      Std.Internal.Parsec.String.Parser Unit

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

                                                                                                                                                                      Equations
                                                                                                                                                                        Instances For
                                                                                                                                                                          source
                                                                                                                                                                          def Lean.Xml.Parser.AttDef :
                                                                                                                                                                          Std.Internal.Parsec.String.Parser Unit

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

                                                                                                                                                                          Equations
                                                                                                                                                                            Instances For
                                                                                                                                                                              source
                                                                                                                                                                              def Lean.Xml.Parser.AttlistDecl :
                                                                                                                                                                              Std.Internal.Parsec.String.Parser Unit

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

                                                                                                                                                                              Equations
                                                                                                                                                                                Instances For
                                                                                                                                                                                  source
                                                                                                                                                                                  def Lean.Xml.Parser.PEReference :
                                                                                                                                                                                  Std.Internal.Parsec.String.Parser Unit

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

                                                                                                                                                                                  Equations
                                                                                                                                                                                    Instances For
                                                                                                                                                                                      source
                                                                                                                                                                                      def Lean.Xml.Parser.EntityValue :
                                                                                                                                                                                      Std.Internal.Parsec.String.Parser String

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

                                                                                                                                                                                      Equations
                                                                                                                                                                                        Instances For
                                                                                                                                                                                          source
                                                                                                                                                                                          def Lean.Xml.Parser.NDataDecl :
                                                                                                                                                                                          Std.Internal.Parsec.String.Parser Unit

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

                                                                                                                                                                                          Equations
                                                                                                                                                                                            Instances For
                                                                                                                                                                                              source
                                                                                                                                                                                              def Lean.Xml.Parser.EntityDef :
                                                                                                                                                                                              Std.Internal.Parsec.String.Parser Unit

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

                                                                                                                                                                                              Equations
                                                                                                                                                                                                Instances For
                                                                                                                                                                                                  source
                                                                                                                                                                                                  def Lean.Xml.Parser.GEDecl :
                                                                                                                                                                                                  Std.Internal.Parsec.String.Parser Unit

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

                                                                                                                                                                                                  Equations
                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                      source
                                                                                                                                                                                                      def Lean.Xml.Parser.PEDef :
                                                                                                                                                                                                      Std.Internal.Parsec.String.Parser Unit

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

                                                                                                                                                                                                      Equations
                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                          source
                                                                                                                                                                                                          def Lean.Xml.Parser.PEDecl :
                                                                                                                                                                                                          Std.Internal.Parsec.String.Parser Unit

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

                                                                                                                                                                                                          Equations
                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                              source
                                                                                                                                                                                                              def Lean.Xml.Parser.EntityDecl :
                                                                                                                                                                                                              Std.Internal.Parsec.String.Parser Unit

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

                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                  source
                                                                                                                                                                                                                  def Lean.Xml.Parser.PublicID :
                                                                                                                                                                                                                  Std.Internal.Parsec.String.Parser Unit

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

                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                      source
                                                                                                                                                                                                                      def Lean.Xml.Parser.NotationDecl :
                                                                                                                                                                                                                      Std.Internal.Parsec.String.Parser Unit

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

                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                          source
                                                                                                                                                                                                                          def Lean.Xml.Parser.markupDecl :
                                                                                                                                                                                                                          Std.Internal.Parsec.String.Parser Unit

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

                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                              source
                                                                                                                                                                                                                              def Lean.Xml.Parser.DeclSep :
                                                                                                                                                                                                                              Std.Internal.Parsec.String.Parser Unit

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

                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                  source
                                                                                                                                                                                                                                  def Lean.Xml.Parser.intSubset :
                                                                                                                                                                                                                                  Std.Internal.Parsec.String.Parser Unit

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

                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                      source
                                                                                                                                                                                                                                      def Lean.Xml.Parser.doctypedecl :
                                                                                                                                                                                                                                      Std.Internal.Parsec.String.Parser Unit

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

                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                          source
                                                                                                                                                                                                                                          def Lean.Xml.Parser.prolog :
                                                                                                                                                                                                                                          Std.Internal.Parsec.String.Parser Unit

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

                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                              source
                                                                                                                                                                                                                                              def Lean.Xml.Parser.Attribute :
                                                                                                                                                                                                                                              Std.Internal.Parsec.String.Parser (String × String)

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

                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                  source
                                                                                                                                                                                                                                                  def Lean.Xml.Parser.elementPrefix :
                                                                                                                                                                                                                                                  Std.Internal.Parsec.String.Parser (Array Content → Element)
                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                      source
                                                                                                                                                                                                                                                      def Lean.Xml.Parser.EmptyElemTag (elem : Array Content → Element) :
                                                                                                                                                                                                                                                      Std.Internal.Parsec.String.Parser Element

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

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

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

                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                              source
                                                                                                                                                                                                                                                              def Lean.Xml.Parser.ETag :
                                                                                                                                                                                                                                                              Std.Internal.Parsec.String.Parser Unit

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

                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                  source
                                                                                                                                                                                                                                                                  def Lean.Xml.Parser.CDStart :
                                                                                                                                                                                                                                                                  Std.Internal.Parsec.String.Parser Unit

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

                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                      source
                                                                                                                                                                                                                                                                      def Lean.Xml.Parser.CDEnd :
                                                                                                                                                                                                                                                                      Std.Internal.Parsec.String.Parser Unit

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

                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                          source
                                                                                                                                                                                                                                                                          def Lean.Xml.Parser.CData :
                                                                                                                                                                                                                                                                          Std.Internal.Parsec.String.Parser String

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

                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                              source
                                                                                                                                                                                                                                                                              def Lean.Xml.Parser.CDSect :
                                                                                                                                                                                                                                                                              Std.Internal.Parsec.String.Parser String

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

                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                  source
                                                                                                                                                                                                                                                                                  def Lean.Xml.Parser.CharData :
                                                                                                                                                                                                                                                                                  Std.Internal.Parsec.String.Parser String

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

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

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

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

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

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

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

                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                          source
                                                                                                                                                                                                                                                                                          def Lean.Xml.parse (s : String) :
                                                                                                                                                                                                                                                                                          Except String Element
                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                            Instances For