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.

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

Decodes the UTF-8 character sequence that starts at a given index in a byte array, or none if index i is out of bounds or is not the start of a valid UTF-8 character.

Equations

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

@[extern lean_string_validate_utf8]

def String.validateUTF8 (a : ByteArray) : Bool

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

Equations

• String.validateUTF8 a = (String.validateUTF8.loop a 0).isSome

@[irreducible]

def String.validateUTF8.loop (a : ByteArray) (i : Nat) : Option Unit

Equations

• String.validateUTF8.loop a i = if i < a.size then do let c ← String.utf8DecodeChar? a i String.validateUTF8.loop a (i + c.utf8Size) else pure ()

@[extern lean_string_from_utf8_unchecked]

def String.fromUTF8 (a : ByteArray) (h : validateUTF8 a = true) : String

Decodes an array of bytes that encode a string as UTF-8 into the corresponding string. Invalid UTF-8 characters in the byte array result in (default : Char), or 'A', in the string.

Equations

• String.fromUTF8 a h = String.fromUTF8.loop a 0 ""

@[irreducible]

def String.fromUTF8.loop (a : ByteArray) (i : Nat) (acc : String) : String

Equations

• String.fromUTF8.loop a i acc = if i < a.size then let c := (String.utf8DecodeChar? a i).getD default; String.fromUTF8.loop a (i + c.utf8Size) (acc.push c) else acc

@[inline]

def String.fromUTF8? (a : ByteArray) : Option String

Decodes an array of bytes that encode a string as UTF-8 into the corresponding string, or returns none if the array is not a valid UTF-8 encoding of a string.

Equations

• String.fromUTF8? a = if h : String.validateUTF8 a = true then some (String.fromUTF8 a h) else none

@[inline]

def String.fromUTF8! (a : ByteArray) : String

Decodes an array of bytes that encode a string as UTF-8 into the corresponding string, or panics if the array is not a valid UTF-8 encoding of a string.

Equations

• String.fromUTF8! a = if h : String.validateUTF8 a = true then String.fromUTF8 a h else panicWithPosWithDecl "Init.Data.String.Extra" "String.fromUTF8!" 126 47 "invalid UTF-8 string"

def String.utf8EncodeChar (c : Char) : List UInt8

Returns the sequence of bytes in a character's UTF-8 encoding.

Equations

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

@[simp]

theorem String.length_utf8EncodeChar (c : Char) : (utf8EncodeChar c).length = c.utf8Size

@[extern lean_string_to_utf8]

def String.toUTF8 (a : String) : ByteArray

Encodes a string in UTF-8 as an array of bytes.

Equations

• a.toUTF8 = { data := { toList := List.flatMap String.utf8EncodeChar a.data } }

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

Accesses the indicated byte in the UTF-8 encoding of a string.

At runtime, this function is implemented by efficient, constant-time code.

Equations

• s.getUtf8Byte n h = s.toUTF8[n]

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

@[irreducible]

def String.crlfToLf.go (text acc : String) (accStop pos : Pos) : String

Equations

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