@[reducible, inline, deprecated ByteArray.utf8DecodeChar? (since := "2025-10-01")]

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

Equations

• String.utf8DecodeChar? a i = a.utf8DecodeChar? i

@[reducible, inline, deprecated ByteArray.validateUTF8 (since := "2025-10-01")]

abbrev String.validateUTF8 (a : ByteArray) : Bool

Checks whether an array of bytes is a valid UTF-8 encoding of a string.

Equations

• String.validateUTF8 a = a.validateUTF8

def String.removeLeadingSpaces (s : String) : String

Consistently de-indents the lines in a string, removing the same amount of leading whitespace from each line such that the least-indented line has no leading whitespace.

The number of leading whitespace characters to remove from each line is determined by counting the number of leading space (' ') and tab ('\t') characters on lines after the first line that also contain non-whitespace characters. No distinction is made between tab and space characters; both count equally.

The least number of leading whitespace characters found is then removed from the beginning of each line. The first line's leading whitespace is not counted when determining how far to de-indent the string, but leading whitespace is removed from it.

Examples:

• "Here:\n fun x =>\n x + 1".removeLeadingSpaces = "Here:\nfun x =>\n x + 1"
• "Here:\n\t\tfun x =>\n\t \tx + 1".removeLeadingSpaces = "Here:\nfun x =>\n \tx + 1"
• "Here:\n\t\tfun x =>\n \n\t \tx + 1".removeLeadingSpaces = "Here:\nfun x =>\n\n \tx + 1"

Equations

• s.removeLeadingSpaces = if (String.findLeadingSpacesSize✝ s == 0) = true then s else String.removeNumLeadingSpaces✝ (String.findLeadingSpacesSize✝¹ s) 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.

This is an optimized version of String.replace text "\r\n" "\n".

Equations

• text.crlfToLf = String.crlfToLf.go✝ text "" 0 0