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
    @[extern lean_string_from_utf8_unchecked]

    Convert a UTF-8 encoded ByteArray string to String. The result is unspecified if a is not properly UTF-8 encoded.

    @[extern lean_string_to_utf8]

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

    @[extern lean_string_get_byte_fast]
    opaque String.getUtf8Byte (s : String) (n : Nat) (h : n < String.utf8ByteSize s) :

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

    @[specialize #[]]

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

    Equations
    Instances For
      @[specialize #[]]
      def String.Iterator.foldUntil {α : Type u_1} (it : String.Iterator) (init : α) (f : αCharOption α) :
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For