Documentation

Lean.Data.Xml.Parser

source
@[inline, reducible]
abbrev Lean.Xml.Parser.LeanChar :
Type
Instances For
    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

    Instances For
      source
      def Lean.Xml.Parser.quote {α : Type} (p : Lean.Parsec α) :
      Lean.Parsec α
      Instances For
        source
        def Lean.Xml.Parser.Char :
        Lean.Parsec Lean.Xml.Parser.LeanChar

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

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

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

          Instances For
            source
            def Lean.Xml.Parser.Eq :
            Lean.Parsec Unit

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

            Instances For
              source
              def Lean.Xml.Parser.NameStartChar :
              Lean.Parsec Lean.Xml.Parser.LeanChar

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

              Instances For
                source
                def Lean.Xml.Parser.NameChar :
                Lean.Parsec Lean.Xml.Parser.LeanChar

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

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

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

                  Instances For
                    source
                    def Lean.Xml.Parser.VersionNum :
                    Lean.Parsec Unit

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

                    Instances For
                      source
                      def Lean.Xml.Parser.VersionInfo :
                      Lean.Parsec Unit

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

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

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

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

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

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

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

                            Instances For
                              source
                              def Lean.Xml.Parser.XMLdecl :
                              Lean.Parsec Unit

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

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

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

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

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

                                  Instances For
                                    source
                                    def Lean.Xml.Parser.PI :
                                    Lean.Parsec Unit

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

                                    Instances For
                                      source
                                      def Lean.Xml.Parser.Misc :
                                      Lean.Parsec Unit

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

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

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

                                        Instances For
                                          source
                                          def Lean.Xml.Parser.PubidChar :
                                          Lean.Parsec Lean.Xml.Parser.LeanChar

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

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

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

                                            Instances For
                                              source
                                              def Lean.Xml.Parser.ExternalID :
                                              Lean.Parsec Unit

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

                                              Instances For
                                                source
                                                def Lean.Xml.Parser.Mixed :
                                                Lean.Parsec Unit

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

                                                Instances For
                                                  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

                                                  Instances For
                                                    source
                                                    def Lean.Xml.Parser.contentspec :
                                                    Lean.Parsec Unit

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

                                                    Instances For
                                                      source
                                                      def Lean.Xml.Parser.elementDecl :
                                                      Lean.Parsec Unit

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

                                                      Instances For
                                                        source
                                                        def Lean.Xml.Parser.StringType :
                                                        Lean.Parsec Unit

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

                                                        Instances For
                                                          source
                                                          def Lean.Xml.Parser.TokenizedType :
                                                          Lean.Parsec Unit

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

                                                          Instances For
                                                            source
                                                            def Lean.Xml.Parser.NotationType :
                                                            Lean.Parsec Unit

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

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

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

                                                              Instances For
                                                                source
                                                                def Lean.Xml.Parser.Enumeration :
                                                                Lean.Parsec Unit

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

                                                                Instances For
                                                                  source
                                                                  def Lean.Xml.Parser.EnumeratedType :
                                                                  Lean.Parsec Unit

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

                                                                  Instances For
                                                                    source
                                                                    def Lean.Xml.Parser.AttType :
                                                                    Lean.Parsec Unit

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

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

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

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

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

                                                                              Instances For
                                                                                source
                                                                                def Lean.Xml.Parser.Reference :
                                                                                Lean.Parsec (Option Lean.Xml.Parser.LeanChar)

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

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

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

                                                                                  Instances For
                                                                                    source
                                                                                    def Lean.Xml.Parser.DefaultDecl :
                                                                                    Lean.Parsec Unit

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

                                                                                    Instances For
                                                                                      source
                                                                                      def Lean.Xml.Parser.AttDef :
                                                                                      Lean.Parsec Unit

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

                                                                                      Instances For
                                                                                        source
                                                                                        def Lean.Xml.Parser.AttlistDecl :
                                                                                        Lean.Parsec Unit

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

                                                                                        Instances For
                                                                                          source
                                                                                          def Lean.Xml.Parser.PEReference :
                                                                                          Lean.Parsec Unit

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

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

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

                                                                                            Instances For
                                                                                              source
                                                                                              def Lean.Xml.Parser.NDataDecl :
                                                                                              Lean.Parsec Unit

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

                                                                                              Instances For
                                                                                                source
                                                                                                def Lean.Xml.Parser.EntityDef :
                                                                                                Lean.Parsec Unit

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

                                                                                                Instances For
                                                                                                  source
                                                                                                  def Lean.Xml.Parser.GEDecl :
                                                                                                  Lean.Parsec Unit

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

                                                                                                  Instances For
                                                                                                    source
                                                                                                    def Lean.Xml.Parser.PEDef :
                                                                                                    Lean.Parsec Unit

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

                                                                                                    Instances For
                                                                                                      source
                                                                                                      def Lean.Xml.Parser.PEDecl :
                                                                                                      Lean.Parsec Unit

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

                                                                                                      Instances For
                                                                                                        source
                                                                                                        def Lean.Xml.Parser.EntityDecl :
                                                                                                        Lean.Parsec Unit

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

                                                                                                        Instances For
                                                                                                          source
                                                                                                          def Lean.Xml.Parser.PublicID :
                                                                                                          Lean.Parsec Unit

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

                                                                                                          Instances For
                                                                                                            source
                                                                                                            def Lean.Xml.Parser.NotationDecl :
                                                                                                            Lean.Parsec Unit

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

                                                                                                            Instances For
                                                                                                              source
                                                                                                              def Lean.Xml.Parser.markupDecl :
                                                                                                              Lean.Parsec Unit

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

                                                                                                              Instances For
                                                                                                                source
                                                                                                                def Lean.Xml.Parser.DeclSep :
                                                                                                                Lean.Parsec Unit

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

                                                                                                                Instances For
                                                                                                                  source
                                                                                                                  def Lean.Xml.Parser.intSubset :
                                                                                                                  Lean.Parsec Unit

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

                                                                                                                  Instances For
                                                                                                                    source
                                                                                                                    def Lean.Xml.Parser.doctypedecl :
                                                                                                                    Lean.Parsec Unit

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

                                                                                                                    Instances For
                                                                                                                      source
                                                                                                                      def Lean.Xml.Parser.prolog :
                                                                                                                      Lean.Parsec Unit

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

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

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

                                                                                                                        Instances For
                                                                                                                          source
                                                                                                                          def Lean.Xml.Parser.elementPrefix :
                                                                                                                          Lean.Parsec (Array Lean.Xml.Content → Lean.Xml.Element)
                                                                                                                          Instances For
                                                                                                                            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

                                                                                                                            Instances For
                                                                                                                              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

                                                                                                                              Instances For
                                                                                                                                source
                                                                                                                                def Lean.Xml.Parser.ETag :
                                                                                                                                Lean.Parsec Unit

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

                                                                                                                                Instances For
                                                                                                                                  source
                                                                                                                                  def Lean.Xml.Parser.CDStart :
                                                                                                                                  Lean.Parsec Unit

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

                                                                                                                                  Instances For
                                                                                                                                    source
                                                                                                                                    def Lean.Xml.Parser.CDEnd :
                                                                                                                                    Lean.Parsec Unit

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

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

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

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

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

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

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

                                                                                                                                          Instances For
                                                                                                                                            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

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