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

@[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 : String.validateUTF8 a = true) : String

Converts a UTF-8 encoded ByteArray string to 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

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

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

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 = c.utf8Size

@[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

@[irreducible, 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

@[irreducible, 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

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. It 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 : String) (acc : String) (accStop : String.Pos) (pos : String.Pos) : String

Equations

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