Documentation

Init.Data.String.Basic

Equations
Instances For
    Equations
    Equations
    @[extern lean_string_dec_lt]
    instance String.decLt (s₁ : String) (s₂ : String) :
    Decidable (s₁ < s₂)
    Equations
    @[extern lean_string_length]
    Equations
    Instances For
      @[extern lean_string_push]

      The internal implementation uses dynamic arrays and will perform destructive updates if the String is not shared.

      Equations
      • String.push x✝ x = match x✝, x with | { data := s }, c => { data := s ++ [c] }
      Instances For
        @[extern lean_string_append]

        The internal implementation uses dynamic arrays and will perform destructive updates if the String is not shared.

        Equations
        • String.append x✝ x = match x✝, x with | { data := a }, { data := b } => { data := a ++ b }
        Instances For

          O(n) in the runtime, where n is the length of the String

          Equations
          Instances For
            Equations
            Instances For
              @[extern lean_string_utf8_get]
              def String.get (s : String) (p : String.Pos) :

              Return character at position p. If p is not a valid position returns (default : Char). See utf8GetAux for the reference implementation.

              Equations
              Instances For
                Equations
                Instances For
                  @[extern lean_string_utf8_get_opt]
                  Equations
                  Instances For
                    @[extern lean_string_utf8_get_bang]

                    Similar to get, but produces a panic error message if p is not a valid String.Pos.

                    Equations
                    Instances For
                      Equations
                      Instances For
                        @[extern lean_string_utf8_set]
                        Equations
                        Instances For
                          def String.modify (s : String) (i : String.Pos) (f : CharChar) :
                          Equations
                          Instances For
                            @[extern lean_string_utf8_next]
                            Equations
                            Instances For
                              Equations
                              Instances For
                                @[extern lean_string_utf8_prev]
                                Equations
                                Instances For
                                  Equations
                                  Instances For
                                    Equations
                                    Instances For
                                      @[extern lean_string_utf8_at_end]
                                      Equations
                                      Instances For
                                        @[extern lean_string_utf8_get_fast]

                                        Similar to get but runtime does not perform bounds check.

                                        Equations
                                        Instances For
                                          @[extern lean_string_utf8_next_fast]

                                          Similar to next but runtime does not perform bounds check.

                                          Equations
                                          Instances For
                                            @[simp]
                                            theorem String.pos_lt_eq (p₁ : String.Pos) (p₂ : String.Pos) :
                                            (p₁ < p₂) = (p₁.byteIdx < p₂.byteIdx)
                                            @[simp]
                                            theorem String.pos_add_char (p : String.Pos) (c : Char) :
                                            (p + c).byteIdx = p.byteIdx + String.csize c
                                            theorem String.lt_next (s : String) (i : String.Pos) :
                                            i.byteIdx < (String.next s i).byteIdx
                                            theorem String.utf8PrevAux_lt_of_pos (cs : List Char) (i : String.Pos) (p : String.Pos) :
                                            p 0(String.utf8PrevAux cs i p).byteIdx < p.byteIdx
                                            theorem String.prev_lt_of_pos (s : String) (i : String.Pos) (h : i 0) :
                                            (String.prev s i).byteIdx < i.byteIdx
                                            def String.posOfAux (s : String) (c : Char) (stopPos : String.Pos) (pos : String.Pos) :
                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              @[inline]
                                              Equations
                                              Instances For
                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  def String.findAux (s : String) (p : CharBool) (stopPos : String.Pos) (pos : String.Pos) :
                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    @[inline]
                                                    def String.find (s : String) (p : CharBool) :
                                                    Equations
                                                    Instances For
                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        @[inline, reducible]
                                                        Equations
                                                        Instances For

                                                          Returns the first position where the two strings differ.

                                                          Equations
                                                          Instances For
                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              @[extern lean_string_utf8_extract]
                                                              Equations
                                                              Instances For
                                                                Equations
                                                                Instances For
                                                                  Equations
                                                                  Instances For
                                                                    @[specialize #[]]
                                                                    def String.splitAux (s : String) (p : CharBool) (b : String.Pos) (i : String.Pos) (r : List String) :
                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For
                                                                      @[specialize #[]]
                                                                      def String.split (s : String) (p : CharBool) :
                                                                      Equations
                                                                      Instances For
                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For
                                                                          Equations
                                                                          Instances For
                                                                            Equations
                                                                            Instances For
                                                                              def String.pushn (s : String) (c : Char) (n : Nat) :
                                                                              Equations
                                                                              Instances For
                                                                                Equations
                                                                                Instances For
                                                                                  Equations
                                                                                  Instances For
                                                                                    Equations
                                                                                    Instances For
                                                                                      Equations
                                                                                      Instances For
                                                                                        Equations
                                                                                        Instances For

                                                                                          Iterator for String. That is, a String and a position in that string.

                                                                                          Instances For
                                                                                            Equations
                                                                                            Instances For
                                                                                              @[inline, reducible]
                                                                                              Equations
                                                                                              Instances For
                                                                                                Equations
                                                                                                Instances For
                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    Equations
                                                                                                    Instances For
                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        Equations
                                                                                                        Instances For
                                                                                                          Equations
                                                                                                          Instances For
                                                                                                            Equations
                                                                                                            Instances For
                                                                                                              Equations
                                                                                                              Instances For
                                                                                                                Equations
                                                                                                                Instances For
                                                                                                                  Equations
                                                                                                                  Instances For
                                                                                                                    Equations
                                                                                                                    Instances For
                                                                                                                      Equations
                                                                                                                      Instances For
                                                                                                                        Equations
                                                                                                                        Instances For
                                                                                                                          def String.offsetOfPosAux (s : String) (pos : String.Pos) (i : String.Pos) (offset : Nat) :
                                                                                                                          Equations
                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                          Instances For
                                                                                                                            Equations
                                                                                                                            Instances For
                                                                                                                              @[specialize #[]]
                                                                                                                              def String.foldlAux {α : Type u} (f : αCharα) (s : String) (stopPos : String.Pos) (i : String.Pos) (a : α) :
                                                                                                                              α
                                                                                                                              Equations
                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                              Instances For
                                                                                                                                @[inline]
                                                                                                                                def String.foldl {α : Type u} (f : αCharα) (init : α) (s : String) :
                                                                                                                                α
                                                                                                                                Equations
                                                                                                                                Instances For
                                                                                                                                  @[specialize #[]]
                                                                                                                                  def String.foldrAux {α : Type u} (f : Charαα) (a : α) (s : String) (i : String.Pos) (begPos : String.Pos) :
                                                                                                                                  α
                                                                                                                                  Equations
                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                  Instances For
                                                                                                                                    @[inline]
                                                                                                                                    def String.foldr {α : Type u} (f : Charαα) (init : α) (s : String) :
                                                                                                                                    α
                                                                                                                                    Equations
                                                                                                                                    Instances For
                                                                                                                                      @[specialize #[]]
                                                                                                                                      def String.anyAux (s : String) (stopPos : String.Pos) (p : CharBool) (i : String.Pos) :
                                                                                                                                      Equations
                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                      Instances For
                                                                                                                                        @[inline]
                                                                                                                                        def String.any (s : String) (p : CharBool) :
                                                                                                                                        Equations
                                                                                                                                        Instances For
                                                                                                                                          @[inline]
                                                                                                                                          def String.all (s : String) (p : CharBool) :
                                                                                                                                          Equations
                                                                                                                                          Instances For
                                                                                                                                            def String.contains (s : String) (c : Char) :
                                                                                                                                            Equations
                                                                                                                                            Instances For
                                                                                                                                              theorem String.utf8SetAux_of_gt (c' : Char) (cs : List Char) {i : String.Pos} {p : String.Pos} :
                                                                                                                                              i > pString.utf8SetAux c' cs i p = cs
                                                                                                                                              theorem String.set_next_add (s : String) (i : String.Pos) (c : Char) (b₁ : Nat) (b₂ : Nat) (h : (String.next s i).byteIdx + b₁ = (String.endPos s).byteIdx + b₂) :
                                                                                                                                              (String.next (String.set s i c) i).byteIdx + b₁ = (String.endPos (String.set s i c)).byteIdx + b₂
                                                                                                                                              theorem String.mapAux_lemma (s : String) (i : String.Pos) (c : Char) (h : ¬String.atEnd s i = true) :
                                                                                                                                              (String.endPos (String.set s i c)).byteIdx - (String.next (String.set s i c) i).byteIdx < (String.endPos s).byteIdx - i.byteIdx
                                                                                                                                              @[specialize #[]]
                                                                                                                                              def String.mapAux (f : CharChar) (i : String.Pos) (s : String) :
                                                                                                                                              Equations
                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                              Instances For
                                                                                                                                                @[inline]
                                                                                                                                                def String.map (f : CharChar) (s : String) :
                                                                                                                                                Equations
                                                                                                                                                Instances For
                                                                                                                                                  Equations
                                                                                                                                                  Instances For
                                                                                                                                                    Equations
                                                                                                                                                    Instances For
                                                                                                                                                      def String.substrEq (s1 : String) (off1 : String.Pos) (s2 : String) (off2 : String.Pos) (sz : Nat) :

                                                                                                                                                      Return true iff the substring of byte size sz starting at position off1 in s1 is equal to that starting at off2 in s2.. False if either substring of that byte size does not exist.

                                                                                                                                                      Equations
                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                      Instances For
                                                                                                                                                        def String.substrEq.loop (s1 : String) (s2 : String) (off1 : String.Pos) (off2 : String.Pos) (stop1 : String.Pos) :
                                                                                                                                                        Equations
                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                        Instances For

                                                                                                                                                          Return true iff p is a prefix of s

                                                                                                                                                          Equations
                                                                                                                                                          Instances For
                                                                                                                                                            def String.replace (s : String) (pattern : String) (replacement : String) :

                                                                                                                                                            Replace all occurrences of pattern in s with replacement.

                                                                                                                                                            Equations
                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                            Instances For
                                                                                                                                                              def String.replace.loop (s : String) (pattern : String) (replacement : String) (hPatt : 0 < (String.endPos pattern).byteIdx) (acc : String) (accStop : String.Pos) (pos : String.Pos) :
                                                                                                                                                              Equations
                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                              Instances For
                                                                                                                                                                @[inline]
                                                                                                                                                                Equations
                                                                                                                                                                Instances For
                                                                                                                                                                  @[inline]
                                                                                                                                                                  Equations
                                                                                                                                                                  Instances For
                                                                                                                                                                    @[inline]
                                                                                                                                                                    Equations
                                                                                                                                                                    • Substring.toIterator x = match x with | { str := s, startPos := b, stopPos := stopPos } => { s := s, i := b }
                                                                                                                                                                    Instances For
                                                                                                                                                                      @[inline]

                                                                                                                                                                      Return the codepoint at the given offset into the substring.

                                                                                                                                                                      Equations
                                                                                                                                                                      Instances For
                                                                                                                                                                        @[inline]

                                                                                                                                                                        Given an offset of a codepoint into the substring, return the offset there of the next codepoint.

                                                                                                                                                                        Equations
                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                        Instances For
                                                                                                                                                                          theorem Substring.lt_next (s : Substring) (i : String.Pos) (h : i.byteIdx < Substring.bsize s) :
                                                                                                                                                                          i.byteIdx < (Substring.next s i).byteIdx
                                                                                                                                                                          @[inline]

                                                                                                                                                                          Given an offset of a codepoint into the substring, return the offset there of the previous codepoint.

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

                                                                                                                                                                                  Return the offset into s of the first occurrence of c in s, or s.bsize if c doesn't occur.

                                                                                                                                                                                  Equations
                                                                                                                                                                                  Instances For
                                                                                                                                                                                    @[inline]
                                                                                                                                                                                    Equations
                                                                                                                                                                                    • Substring.drop x✝ x = match x✝, x with | ss@h:{ str := s, startPos := b, stopPos := e }, n => { str := s, startPos := b + Substring.nextn ss n 0, stopPos := e }
                                                                                                                                                                                    Instances For
                                                                                                                                                                                      @[inline]
                                                                                                                                                                                      Equations
                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                      Instances For
                                                                                                                                                                                        @[inline]
                                                                                                                                                                                        Equations
                                                                                                                                                                                        • Substring.take x✝ x = match x✝, x with | ss@h:{ str := s, startPos := b, stopPos := stopPos }, n => { str := s, startPos := b, stopPos := b + Substring.nextn ss n 0 }
                                                                                                                                                                                        Instances For
                                                                                                                                                                                          @[inline]
                                                                                                                                                                                          Equations
                                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                                          Instances For
                                                                                                                                                                                            @[inline]
                                                                                                                                                                                            Equations
                                                                                                                                                                                            • Substring.atEnd x✝ x = match x✝, x with | { str := str, startPos := b, stopPos := e }, p => b + p == e
                                                                                                                                                                                            Instances For
                                                                                                                                                                                              @[inline]
                                                                                                                                                                                              Equations
                                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                                              Instances For
                                                                                                                                                                                                Equations
                                                                                                                                                                                                Instances For
                                                                                                                                                                                                  Equations
                                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                    @[inline]
                                                                                                                                                                                                    def Substring.foldl {α : Type u} (f : αCharα) (init : α) (s : Substring) :
                                                                                                                                                                                                    α
                                                                                                                                                                                                    Equations
                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                      @[inline]
                                                                                                                                                                                                      def Substring.foldr {α : Type u} (f : Charαα) (init : α) (s : Substring) :
                                                                                                                                                                                                      α
                                                                                                                                                                                                      Equations
                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                        @[inline]
                                                                                                                                                                                                        def Substring.any (s : Substring) (p : CharBool) :
                                                                                                                                                                                                        Equations
                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                          @[inline]
                                                                                                                                                                                                          def Substring.all (s : Substring) (p : CharBool) :
                                                                                                                                                                                                          Equations
                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                            Equations
                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                              @[specialize #[]]
                                                                                                                                                                                                              def Substring.takeWhileAux (s : String) (stopPos : String.Pos) (p : CharBool) (i : String.Pos) :
                                                                                                                                                                                                              Equations
                                                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                @[inline]
                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                  @[inline]
                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                    @[specialize #[]]
                                                                                                                                                                                                                    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
                                                                                                                                                                                                                        @[inline]
                                                                                                                                                                                                                        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
                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                def Substring.beq (ss1 : Substring) (ss2 : Substring) :
                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                  @[inline]
                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                    @[inline]
                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                      Instances For