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.
Instances For
@[extern lean_string_validate_utf8]
Returns true if the given byte array consists of valid UTF-8.
Instances For
@[irreducible]
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 ()
Instances For
@[irreducible]
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
Instances For
@[inline]
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
Instances For
@[inline]
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!" 100 47 "invalid UTF-8 string"
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[extern lean_string_to_utf8]
Converts the given String
to a UTF-8 encoded byte array.
Equations
- a.toUTF8 = { data := { toList := a.data.flatMap String.utf8EncodeChar } }
Instances For
@[irreducible, specialize #[]]
Advance the given iterator until the predicate returns true or the end of the string is reached.
Instances For
@[irreducible, specialize #[]]
def
String.Iterator.foldUntil
{α : Type u_1}
(it : String.Iterator)
(init : α)
(f : α → Char → Option α)
:
Instances For
Equations
- s.removeLeadingSpaces = if (String.findLeadingSpacesSize✝ s == 0) = true then s else String.removeNumLeadingSpaces✝ (String.findLeadingSpacesSize✝ s) s
Instances For
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"
.
Instances For
@[irreducible]
Equations
- One or more equations did not get rendered due to their size.