def String.toNat! (s : String) : Nat

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.

@[extern lean_string_from_utf8_unchecked]

opaque String.fromUTF8Unchecked (a : ByteArray) : String

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]

opaque String.toUTF8 (a : String) : ByteArray

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) : UInt8

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

theorem String.Iterator.sizeOf_next_lt_of_hasNext (i : String.Iterator) (h : String.Iterator.hasNext i = true) : sizeOf (String.Iterator.next i) < sizeOf i

theorem String.Iterator.sizeOf_next_lt_of_atEnd (i : String.Iterator) (h : ¬String.Iterator.atEnd i = true) : sizeOf (String.Iterator.next i) < sizeOf i

@[specialize #[]]

def String.Iterator.find (it : String.Iterator) (p : Char → Bool) : String.Iterator

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

Equations

• String.Iterator.find it p = if String.Iterator.atEnd it = true then it else if p (String.Iterator.curr it) = true then it else String.Iterator.find (String.Iterator.next it) p

@[specialize #[]]

def String.Iterator.foldUntil {α : Type u_1} (it : String.Iterator) (init : α) (f : α → Char → Option α) : α × String.Iterator

Equations

• One or more equations did not get rendered due to their size.