Documentation

Init.Data.String.Extra

Interpret the string as the decimal representation of a natural number.

Panics if the string is not a string of digits.

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

      Returns true if the given byte array consists of valid UTF-8.

      Instances For
        @[irreducible]
        Equations
        Instances For
          @[extern lean_string_from_utf8_unchecked]

          Converts a UTF-8 encoded ByteArray string to String.

          Instances For
            @[irreducible]
            Equations
            Instances For
              @[inline]

              Converts a UTF-8 encoded ByteArray string to String, or returns none if a is not properly UTF-8 encoded.

              Equations
              Instances For
                @[inline]

                Converts a UTF-8 encoded ByteArray string to String, or panics if a is not properly UTF-8 encoded.

                Equations
                Instances For
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[simp]
                    theorem String.length_utf8EncodeChar (c : Char) :
                    (String.utf8EncodeChar c).length = c.utf8Size
                    @[extern lean_string_to_utf8]

                    Converts the given String to a UTF-8 encoded byte array.

                    Equations
                    Instances For
                      @[simp]
                      theorem String.size_toUTF8 (s : String) :
                      s.toUTF8.size = s.utf8ByteSize
                      @[extern lean_string_get_byte_fast]
                      def String.getUtf8Byte (s : String) (n : Nat) (h : n < s.utf8ByteSize) :

                      Accesses a byte in the UTF-8 encoding of the String. O(1)

                      Equations
                      • s.getUtf8Byte n h = s.toUTF8[n]
                      Instances For
                        @[irreducible, specialize #[]]

                        Advance the given iterator until the predicate returns true or the end of the string is reached.

                        Instances For
                          @[irreducible, specialize #[]]
                          def String.Iterator.foldUntil {α : Type u_1} (it : String.Iterator) (init : α) (f : αCharOption α) :
                          Instances For

                            Replaces each \r\n with \n to normalize line endings, but does not validate that there are no isolated \r characters. It is an optimized version of String.replace text "\r\n" "\n".

                            Instances For
                              @[irreducible]
                              def String.crlfToLf.go (text acc : String) (accStop pos : String.Pos) :
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For