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
                                                      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 over the characters (Char) of a String.

                                                                                          Typically created by s.iter, where s is a String.

                                                                                          An iterator is valid if the position i is valid for the string s, meaning 0 ≤ i ≤ s.endPos and i lies on a UTF8 byte boundary. If i = s.endPos, the iterator is at the end of the string.

                                                                                          Most operations on iterators return arbitrary values if the iterator is not valid. The functions in the String.Iterator API should rule out the creation of invalid iterators, with two exceptions:

                                                                                          • s : String

                                                                                            The string the iterator is for.

                                                                                          • The current position.

                                                                                            This position is not necessarily valid for the string, for instance if one keeps calling Iterator.next when Iterator.atEnd is true. If the position is not valid, then the current character is (default : Char), similar to String.get on an invalid position.

                                                                                          Instances For

                                                                                            Creates an iterator at the beginning of a string.

                                                                                            Equations
                                                                                            Instances For
                                                                                              @[inline, reducible]

                                                                                              Creates an iterator at the beginning of a string.

                                                                                              Equations
                                                                                              Instances For

                                                                                                The size of a string iterator is the number of bytes remaining.

                                                                                                Equations

                                                                                                The string the iterator is for.

                                                                                                Equations
                                                                                                Instances For

                                                                                                  Number of bytes remaining in the iterator.

                                                                                                  Equations
                                                                                                  Instances For

                                                                                                    The current position.

                                                                                                    This position is not necessarily valid for the string, for instance if one keeps calling Iterator.next when Iterator.atEnd is true. If the position is not valid, then the current character is (default : Char), similar to String.get on an invalid position.

                                                                                                    Equations
                                                                                                    Instances For

                                                                                                      The character at the current position.

                                                                                                      On an invalid position, returns (default : Char).

                                                                                                      Equations
                                                                                                      Instances For

                                                                                                        Moves the iterator's position forward by one character, unconditionally.

                                                                                                        It is only valid to call this function if the iterator is not at the end of the string, i.e. Iterator.atEnd is false; otherwise, the resulting iterator will be invalid.

                                                                                                        Equations
                                                                                                        Instances For

                                                                                                          Decreases the iterator's position.

                                                                                                          If the position is zero, this function is the identity.

                                                                                                          Equations
                                                                                                          Instances For

                                                                                                            True if the iterator is past the string's last character.

                                                                                                            Equations
                                                                                                            Instances For

                                                                                                              True if the iterator is not past the string's last character.

                                                                                                              Equations
                                                                                                              Instances For

                                                                                                                True if the position is not zero.

                                                                                                                Equations
                                                                                                                Instances For

                                                                                                                  Replaces the current character in the string.

                                                                                                                  Does nothing if the iterator is at the end of the string. If the iterator contains the only reference to its string, this function will mutate the string in-place instead of allocating a new one.

                                                                                                                  Equations
                                                                                                                  Instances For

                                                                                                                    Moves the iterator's position to the end of the string.

                                                                                                                    Note that i.toEnd.atEnd is always true.

                                                                                                                    Equations
                                                                                                                    Instances For

                                                                                                                      Extracts the substring between the positions of two iterators.

                                                                                                                      Returns the empty string if the iterators are for different strings, or if the position of the first iterator is past the position of the second iterator.

                                                                                                                      Equations
                                                                                                                      Instances For

                                                                                                                        Moves the iterator's position several characters forward.

                                                                                                                        The resulting iterator is only valid if the number of characters to skip is less than or equal to the number of characters left in the iterator.

                                                                                                                        Equations
                                                                                                                        Instances For

                                                                                                                          The remaining characters in an iterator, as a string.

                                                                                                                          Equations
                                                                                                                          Instances For

                                                                                                                            Moves the iterator's position several characters forward.

                                                                                                                            The resulting iterator is only valid if the number of characters to skip is less than or equal to the number of characters left in the iterator.

                                                                                                                            Equations
                                                                                                                            Instances For

                                                                                                                              Moves the iterator's position several characters back.

                                                                                                                              If asked to go back more characters than available, stops at the beginning of the string.

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

                                                                                                                                                                      Return the beginning of the line that contains character pos.

                                                                                                                                                                      Equations
                                                                                                                                                                      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