Documentation

Init.Data.String.Extra

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.
Equations
  • One or more equations did not get rendered due to their size.
@[extern lean_string_validate_utf8]

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

Equations
@[irreducible]
Equations
@[extern lean_string_from_utf8_unchecked]

Converts a UTF-8 encoded ByteArray string to String.

Equations
@[irreducible]
Equations
@[inline]

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

Equations
@[inline]

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

Equations
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]

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

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

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

Equations
  • s.getUtf8Byte n h = s.toUTF8[n]
@[irreducible, specialize #[]]

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 : Iterator) (init : α) (f : αCharOption α) :
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)

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
@[irreducible]
def String.crlfToLf.go (text acc : String) (accStop pos : Pos) :
Equations
  • One or more equations did not get rendered due to their size.