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.
Returns true if the given byte array consists of valid UTF-8.
Equations
- String.validateUTF8 a = (String.validateUTF8.loop a 0).isSome
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 ()
Converts a UTF-8 encoded ByteArray
string to String
.
Equations
- String.fromUTF8 a h = String.fromUTF8.loop a 0 ""
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
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
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"
Equations
- One or more equations did not get rendered due to their size.
Converts the given String
to a UTF-8 encoded byte array.
Equations
- a.toUTF8 = { data := { toList := a.data.flatMap String.utf8EncodeChar } }
Advance the given iterator until the predicate returns true or the end of the string is reached.
Equations
- s.removeLeadingSpaces = if (String.findLeadingSpacesSize✝ s == 0) = true then s else String.removeNumLeadingSpaces✝ (String.findLeadingSpacesSize✝ s) s
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
Equations
- One or more equations did not get rendered due to their size.