Documentation

Lean.Data.Xml.Parser

@[inline, reducible]
Equations
Instances For

    consume a newline character sequence pretending, that we read '\n'. As per spec: https://www.w3.org/TR/xml/#sec-line-ends

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                                              Equations
                                              Instances For

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

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

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

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

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

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

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

                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          @[inline]
                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            def Lean.Xml.Parser.digitsToNat (base : Nat) (digits : Array Nat) :
                                                            Equations
                                                            Instances For

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                                                                                              Equations
                                                                                              Instances For

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

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

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

                                                                                                  Equations
                                                                                                  Instances For

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

                                                                                                    Equations
                                                                                                    Instances For

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

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

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

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

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

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