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
                                            partial def String.posOfAux (s : String) (c : Char) (stopPos : String.Pos) (pos : String.Pos) :
                                            @[inline]
                                            Equations
                                            Instances For
                                              Equations
                                              Instances For
                                                partial def String.findAux (s : String) (p : CharBool) (stopPos : String.Pos) (pos : String.Pos) :
                                                @[inline]
                                                def String.find (s : String) (p : CharBool) :
                                                Equations
                                                Instances For
                                                  partial def String.revFindAux (s : String) (p : CharBool) (pos : String.Pos) :
                                                  Equations
                                                  Instances For
                                                    @[inline]
                                                    Equations
                                                    Instances For

                                                      Returns the first position where the two strings differ.

                                                      Equations
                                                      Instances For
                                                        partial def String.firstDiffPos.loop (a : String) (b : String) (stopPos : String.Pos) (i : String.Pos) :
                                                        @[extern lean_string_utf8_extract]
                                                        Equations
                                                        Instances For
                                                          Equations
                                                          Instances For
                                                            Equations
                                                            Instances For
                                                              @[specialize #[]]
                                                              partial def String.splitAux (s : String) (p : CharBool) (b : String.Pos) (i : String.Pos) (r : List String) :
                                                              @[specialize #[]]
                                                              def String.split (s : String) (p : CharBool) :
                                                              Equations
                                                              Instances For
                                                                partial def String.splitOnAux (s : String) (sep : String) (b : String.Pos) (i : String.Pos) (j : String.Pos) (r : List String) :
                                                                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]
                                                                                    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
                                                                                                                partial def String.offsetOfPosAux (s : String) (pos : String.Pos) (i : String.Pos) (offset : Nat) :
                                                                                                                Equations
                                                                                                                Instances For
                                                                                                                  @[specialize #[]]
                                                                                                                  def String.foldlAux {α : Type u} (f : αCharα) (s : String) (stopPos : String.Pos) (i : String.Pos) (a : α) :
                                                                                                                  α
                                                                                                                  Equations
                                                                                                                  Instances For
                                                                                                                    partial def String.foldlAux.loop {α : Type u} (f : αCharα) (s : String) (stopPos : String.Pos) (i : String.Pos) (a : α) :
                                                                                                                    α
                                                                                                                    @[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) (stopPos : String.Pos) (i : String.Pos) :
                                                                                                                      α
                                                                                                                      Equations
                                                                                                                      Instances For
                                                                                                                        partial def String.foldrAux.loop {α : Type u} (f : Charαα) (a : α) (s : String) (stopPos : String.Pos) (i : String.Pos) :
                                                                                                                        α
                                                                                                                        @[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
                                                                                                                            partial def String.anyAux.loop (s : String) (stopPos : String.Pos) (p : CharBool) (i : String.Pos) :
                                                                                                                            @[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
                                                                                                                                  @[specialize #[]]
                                                                                                                                  partial def String.mapAux (f : CharChar) (i : String.Pos) (s : String) :
                                                                                                                                  @[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
                                                                                                                                          partial def String.substrEq.loop (s1 : String) (s2 : String) (off1 : String.Pos) (off2 : String.Pos) (stop1 : String.Pos) :

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

                                                                                                                                            Equations
                                                                                                                                            Instances For
                                                                                                                                              partial def String.replace.loop (s : String) (pattern : String) (replacement : String) (acc : String) (accStop : String.Pos) (pos : String.Pos) :
                                                                                                                                              @[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
                                                                                                                                                      • Substring.next x x = match x, x with | { str := s, startPos := b, stopPos := e }, p => let absP := b + p; if absP = e then p else { byteIdx := (String.next s absP).byteIdx - b.byteIdx }
                                                                                                                                                      Instances For
                                                                                                                                                        @[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
                                                                                                                                                          @[inline]
                                                                                                                                                          Equations
                                                                                                                                                          Instances For
                                                                                                                                                            @[inline]

                                                                                                                                                            Return the offset into s of the first occurence 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
                                                                                                                                                                            @[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
                                                                                                                                                                                      @[inline]
                                                                                                                                                                                      Equations
                                                                                                                                                                                      Instances For
                                                                                                                                                                                        @[inline]
                                                                                                                                                                                        Equations
                                                                                                                                                                                        Instances For
                                                                                                                                                                                          @[inline]
                                                                                                                                                                                          Equations
                                                                                                                                                                                          Instances For
                                                                                                                                                                                            @[inline]
                                                                                                                                                                                            Equations
                                                                                                                                                                                            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