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.

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

Equations

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

@[extern lean_string_validate_utf8]

def String.validateUTF8 (a : ByteArray) : Bool

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

Equations

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

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 + String.csize c) else pure ()

@[extern lean_string_from_utf8]

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

Converts a UTF-8 encoded ByteArray string to String.

Equations

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

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 + String.csize c) (acc.push c) else acc

@[inline]

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

Converts a UTF-8 encoded ByteArray string to String, or returns none if a is not properly UTF-8 encoded.

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

Converts a UTF-8 encoded ByteArray string to String, or panics if a is not properly UTF-8 encoded.

Equations

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

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

Equations

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

@[simp]

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

@[extern lean_string_to_utf8]

def String.toUTF8 (a : String) : ByteArray

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

Equations

• a.toUTF8 = { data := { data := a.data.bind String.utf8EncodeChar } }

@[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 a byte in the UTF-8 encoding of the String. O(1)

Equations

• s.getUtf8Byte n h = s.toUTF8.get ⟨n, ⋯⟩

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

theorem String.Iterator.sizeOf_next_lt_of_atEnd (i : String.Iterator) (h : ¬i.atEnd = true) : sizeOf i.next < 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

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

@[specialize #[]]

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

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

Equations

• s.removeLeadingSpaces = let n := String.findLeadingSpacesSize s; if (n == 0) = true then s else String.removeNumLeadingSpaces n s