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
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[extern lean_string_validate_utf8]

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

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

          Converts a UTF-8 encoded ByteArray string to String.

          Equations
          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.get n,
                      Instances For
                        @[irreducible, specialize #[]]

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

                        Equations
                        • it.find p = if it.atEnd = true then it else if p it.curr = true then it else it.next.find p
                        Instances For
                          @[irreducible, specialize #[]]
                          def String.Iterator.foldUntil {α : Type u_1} (it : String.Iterator) (init : α) (f : αCharOption α) :
                          Equations
                          • it.foldUntil init f = if it.atEnd = true then (init, it) else match f init it.curr with | some a => it.next.foldUntil a f | x => (init, it)
                          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".

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