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

Interprets a string as the decimal representation of a natural number, returning it. Panics if the string does not contain a decimal natural number.

A string can be interpreted as a decimal natural number if it is not empty and all the characters in it are digits.

Use String.isNat to check whether String.toNat! would return a value. String.toNat? is a safer alternative that returns none instead of panicking when the string is not a natural number.

Examples:

• "0".toNat! = 0
• "5".toNat! = 5
• "587".toNat! = 587

Equations

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

@[reducible, inline, deprecated ByteArray.utf8DecodeChar? (since := "2025-10-01")]

abbrev String.utf8DecodeChar? (a : ByteArray) (i : Nat) : Option Char

Equations

• String.utf8DecodeChar? a i = a.utf8DecodeChar? i

@[reducible, inline, deprecated ByteArray.validateUTF8 (since := "2025-10-01")]

abbrev String.validateUTF8 (a : ByteArray) : Bool

Checks whether an array of bytes is a valid UTF-8 encoding of a string.

Equations

• String.validateUTF8 a = a.validateUTF8

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

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

@[irreducible, specialize #[]]

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

Moves the iterator forward until the Boolean predicate p returns true for the iterator's current character or until the end of the string is reached. Does nothing if the current character already satisfies p.

Equations

• it.find p = if it.atEnd = true then it else if p it.curr = true then it else it.next.find p

@[irreducible, specialize #[]]

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

Iterates over a string, updating a state at each character using the provided function f, until f returns none. Begins with the state init. Returns the state and character for which f returns none.

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)

def String.removeLeadingSpaces (s : String) : String

Consistently de-indents the lines in a string, removing the same amount of leading whitespace from each line such that the least-indented line has no leading whitespace.

The number of leading whitespace characters to remove from each line is determined by counting the number of leading space (' ') and tab ('\t') characters on lines after the first line that also contain non-whitespace characters. No distinction is made between tab and space characters; both count equally.

The least number of leading whitespace characters found is then removed from the beginning of each line. The first line's leading whitespace is not counted when determining how far to de-indent the string, but leading whitespace is removed from it.

Examples:

• "Here:\n fun x =>\n x + 1".removeLeadingSpaces = "Here:\nfun x =>\n x + 1"
• "Here:\n\t\tfun x =>\n\t \tx + 1".removeLeadingSpaces = "Here:\nfun x =>\n \tx + 1"
• "Here:\n\t\tfun x =>\n \n\t \tx + 1".removeLeadingSpaces = "Here:\nfun x =>\n\n \tx + 1"

Equations

• s.removeLeadingSpaces = if (String.findLeadingSpacesSize✝ s == 0) = true then s else String.removeNumLeadingSpaces✝ (String.findLeadingSpacesSize✝¹ s) s

def String.crlfToLf (text : String) : String

Replaces each \r\n with \n to normalize line endings, but does not validate that there are no isolated \r characters.

This is an optimized version of String.replace text "\r\n" "\n".

Equations

• text.crlfToLf = String.crlfToLf.go✝ text "" 0 0