@[inline]

def String.drop (s : String) (n : Nat) : Slice

Returns a String.Slice obtained by removing the specified number of characters (Unicode code points) from the start of the string.

If n is greater than s.length, returns an empty slice.

This is a cheap operation because it does not allocate a new string to hold the result. To convert the result into a string, use String.Slice.copy.

Examples:

• "red green blue".drop 4 == "green blue".toSlice

• "red green blue".drop 10 == "blue".toSlice

• "red green blue".drop 50 == "".toSlice

• "مرحبا بالعالم".drop 3 == "با بالعالم".toSlice

@[export lean_string_drop]

def String.Internal.dropImpl (s : String) (n : Nat) : String

@[inline]

def String.dropEnd (s : String) (n : Nat) : Slice

Returns a String.Slice obtained by removing the specified number of characters (Unicode code points) from the end of the string.

If n is greater than s.length, returns an empty slice.

This is a cheap operation because it does not allocate a new string to hold the result. To convert the result into a string, use String.Slice.copy.

Examples:

• "red green blue".dropEnd 5 == "red green".toSlice

• "red green blue".dropEnd 11 == "red".toSlice

• "red green blue".dropEnd 50 == "".toSlice

• "مرحبا بالعالم".dropEnd 3 == "مرحبا بالع".toSlice

@[deprecated String.dropEnd (since := "2025-11-14")]

def String.dropRight (s : String) (n : Nat) : String

@[deprecated String.Slice.dropEnd (since := "2025-11-20")]

def String.Slice.dropRight (s : Slice) (n : Nat) : Slice

@[export lean_string_dropright]

def String.Internal.dropRightImpl (s : String) (n : Nat) : String

@[inline]

def String.take (s : String) (n : Nat) : Slice

Returns a String.Slice that contains the first n characters (Unicode code points) of s.

If n is greater than s.length, returns s.toSlice.

This is a cheap operation because it does not allocate a new string to hold the result. To convert the result into a string, use String.Slice.copy.

Examples:

• "red green blue".take 3 == "red".toSlice

• "red green blue".take 1 == "r".toSlice

• "red green blue".take 0 == "".toSlice

• "red green blue".take 100 == "red green blue".toSlice

• "مرحبا بالعالم".take 5 == "مرحبا".toSlice

@[inline]

def String.takeEnd (s : String) (n : Nat) : Slice

Returns a String.Slice that contains the last n characters (Unicode code points) of s.

If n is greater than s.length, returns s.toSlice.

This is a cheap operation because it does not allocate a new string to hold the result. To convert the result into a string, use String.Slice.copy.

Examples:

• "red green blue".takeEnd 4 == "blue".toSlice

• "red green blue".takeEnd 1 == "e".toSlice

• "red green blue".takeEnd 0 == "".toSlice

• "red green blue".takeEnd 100 == "red green blue".toSlice

• "مرحبا بالعالم".takeEnd 5 == "لعالم".toSlice

@[deprecated String.takeEnd (since := "2025-11-14")]

def String.takeRight (s : String) (n : Nat) : String

@[deprecated String.Slice.takeEnd (since := "2025-11-20")]

def String.Slice.takeRight (s : Slice) (n : Nat) : Slice

@[inline]

def String.takeWhile {ρ : Type} (s : String) (pat : ρ) [Slice.Pattern.ForwardPattern pat] : Slice

Creates a string slice that contains the longest prefix of s in which pat matched (potentially repeatedly).

This is a cheap operation because it does not allocate a new string to hold the result. To convert the result into a string, use String.Slice.copy.

This function is generic over all currently supported patterns.

Examples:

• "red green blue".takeWhile Char.isLower == "red".toSlice

• "red green blue".takeWhile 'r' == "r".toSlice

• "red red green blue".takeWhile "red " == "red red ".toSlice

• "red green blue".takeWhile (fun (_ : Char) => true) == "red green blue".toSlice

@[inline]

def String.dropWhile {ρ : Type} (s : String) (pat : ρ) [Slice.Pattern.ForwardPattern pat] : Slice

Creates a string slice by removing the longest prefix from s in which pat matched (potentially repeatedly).

This is a cheap operation because it does not allocate a new string to hold the result. To convert the result into a string, use String.Slice.copy.

This function is generic over all currently supported patterns.

Examples:

• "red green blue".dropWhile Char.isLower == " green blue".toSlice

• "red green blue".dropWhile 'r' == "ed green blue".toSlice

• "red red green blue".dropWhile "red " == "green blue".toSlice

• "red green blue".dropWhile (fun (_ : Char) => true) == "".toSlice

@[inline]

def String.takeEndWhile {ρ : Type} (s : String) (pat : ρ) [Slice.Pattern.BackwardPattern pat] : Slice

Creates a string slice that contains the longest suffix of s in which pat matched (potentially repeatedly).

This is a cheap operation because it does not allocate a new string to hold the result. To convert the result into a string, use String.Slice.copy.

This function is generic over all currently supported patterns.

Examples:

• "red green blue".takeEndWhile Char.isLower == "blue".toSlice

• "red green blue".takeEndWhile 'e' == "e".toSlice

• "red green blue".takeEndWhile (fun (_ : Char) => true) == "red green blue".toSlice

@[deprecated String.takeEndWhile (since := "2025-11-17")]

def String.takeRightWhile (s : String) (p : Char → Bool) : String

@[deprecated String.Slice.takeEndWhile (since := "2025-11-20")]

def String.Slice.takeRightWhile (s : Slice) (p : Char → Bool) : Slice

@[inline]

def String.dropEndWhile {ρ : Type} (s : String) (pat : ρ) [Slice.Pattern.BackwardPattern pat] : Slice

Creates a new string by removing the longest suffix from s in which pat matches (potentially repeatedly).

This is a cheap operation because it does not allocate a new string to hold the result. To convert the result into a string, use String.Slice.copy.

This function is generic over all currently supported patterns.

Examples:

• "red green blue".dropEndWhile Char.isLower == "red green ".toSlice

• "red green blue".dropEndWhile 'e' == "red green blu".toSlice

• "red green blue".dropEndWhile (fun (_ : Char) => true) == "".toSlice

@[deprecated String.dropEndWhile (since := "2025-11-17")]

def String.dropRightWhile (s : String) (p : Char → Bool) : String

@[deprecated String.Slice.dropEndWhile (since := "2025-11-20")]

def String.Slice.dropRightWhile (s : Slice) (p : Char → Bool) : Slice

@[inline]

def String.skipPrefix? {ρ : Type} (s : String) (pat : ρ) [Slice.Pattern.ForwardPattern pat] : Option s.Pos

If pat matches a prefix of s, returns the position at the start of the remainder. Returns none otherwise.

This function is generic over all currently supported patterns.

@[inline]

def String.skipPrefixWhile {ρ : Type} (s : String) (pat : ρ) [Slice.Pattern.ForwardPattern pat] : s.Pos

Returns the position after the longest prefix of s for which pat matches (potentially repeatedly).

@[inline]

def String.Pos.skip? {ρ : Type} {s : String} (pos : s.Pos) (pat : ρ) [Slice.Pattern.ForwardPattern pat] : Option s.Pos

If pat matches at pos, returns the position after the end of the match. Returns none otherwise.

This function is generic over all currently supported patterns.

@[inline]

def String.Pos.skipWhile {ρ : Type} {s : String} (pos : s.Pos) (pat : ρ) [Slice.Pattern.ForwardPattern pat] : s.Pos

Advances pos as long as pat matches.

@[inline]

def String.startsWith {ρ : Type} (s : String) (pat : ρ) [Slice.Pattern.ForwardPattern pat] : Bool

Checks whether the first string (s) begins with the pattern (pat).

String.isPrefixOf is a version that takes the potential prefix before the string.

Examples:

• "red green blue".startsWith "red" = true

• "red green blue".startsWith "green" = false

• "red green blue".startsWith "" = true

• "red green blue".startsWith 'r' = true

• "red green blue".startsWith Char.isLower = true

@[inline]

def String.isPrefixOf (p s : String) : Bool

Checks whether the second string (s) begins with a prefix (p).

This function is generic over all currently supported patterns.

String.startsWith is a version that takes the potential prefix after the string.

Examples:

• "red".isPrefixOf "red green blue" = true

• "green".isPrefixOf "red green blue" = false

• "".isPrefixOf "red green blue" = true

@[export lean_string_isprefixof]

def String.Internal.isPrefixOfImpl (p s : String) : Bool

@[inline]

def String.endsWith {ρ : Type} (s : String) (pat : ρ) [Slice.Pattern.BackwardPattern pat] : Bool

Checks whether the string (s) ends with the pattern (pat).

This function is generic over all currently supported patterns.

Examples:

• "red green blue".endsWith "blue" = true

• "red green blue".endsWith "green" = false

• "red green blue".endsWith "" = true

• "red green blue".endsWith 'e' = true

• "red green blue".endsWith Char.isLower = true

@[inline]

def String.skipSuffix? {ρ : Type} (s : String) (pat : ρ) [Slice.Pattern.BackwardPattern pat] : Option s.Pos

If pat matches a suffix of s, returns the position at the beginning of the suffix. Returns none otherwise.

This function is generic over all currently supported patterns.

@[inline]

def String.skipSuffixWhile {ρ : Type} (s : String) (pat : ρ) [Slice.Pattern.BackwardPattern pat] : s.Pos

Returns the position at the start of the longest suffix of s for which pat matches (potentially repeatedly).

@[inline]

def String.Pos.revSkip? {ρ : Type} {s : String} (pos : s.Pos) (pat : ρ) [Slice.Pattern.BackwardPattern pat] : Option s.Pos

If pat matches at pos, returns the position after the end of the match. Returns none otherwise.

This function is generic over all currently supported patterns.

@[inline]

def String.Pos.revSkipWhile {ρ : Type} {s : String} (pos : s.Pos) (pat : ρ) [Slice.Pattern.BackwardPattern pat] : s.Pos

Rewinds pos as long as pat matches.

@[inline]

def String.trimAsciiEnd (s : String) : Slice

Removes trailing whitespace from a string by returning a slice whose end position is the last non-whitespace character, or the start position if there is no non-whitespace character.

“Whitespace” is defined as characters for which Char.isWhitespace returns true.

Examples:

• "abc".trimAsciiEnd == "abc".toSlice

• " abc".trimAsciiEnd == " abc".toSlice

• "abc \t ".trimAsciiEnd == "abc".toSlice

• " abc ".trimAsciiEnd == " abc".toSlice

• "abc\ndef\n".trimAsciiEnd == "abc\ndef".toSlice

@[deprecated String.trimAsciiEnd (since := "2025-11-17")]

def String.trimRight (s : String) : String

@[deprecated String.Slice.trimAsciiEnd (since := "2025-11-20")]

def String.Slice.trimRight (s : Slice) : Slice

@[inline]

def String.trimAsciiStart (s : String) : Slice

Removes leading whitespace from a string by returning a slice whose start position is the first non-whitespace character, or the end position if there is no non-whitespace character.

“Whitespace” is defined as characters for which Char.isWhitespace returns true.

Examples:

• "abc".trimAsciiStart == "abc".toSlice

• " abc".trimAsciiStart == "abc".toSlice

• "abc \t ".trimAsciiStart == "abc \t ".toSlice

• " abc ".trimAsciiStart == "abc ".toSlice

• "abc\ndef\n".trimAsciiStart == "abc\ndef\n".toSlice

@[deprecated String.trimAsciiStart (since := "2025-11-17")]

def String.trimLeft (s : String) : String

@[deprecated String.Slice.trimAsciiStart (since := "2025-11-20")]

def String.Slice.trimLeft (s : Slice) : Slice

@[inline]

def String.trimAscii (s : String) : Slice

Removes leading and trailing whitespace from a string.

“Whitespace” is defined as characters for which Char.isWhitespace returns true.

Examples:

• "abc".trimAscii == "abc".toSlice

• " abc".trimAscii == "abc".toSlice

• "abc \t ".trimAscii == "abc".toSlice

• " abc ".trimAscii == "abc".toSlice

• "abc\ndef\n".trimAscii == "abc\ndef".toSlice

@[deprecated String.trimAscii (since := "2025-11-17")]

def String.trim (s : String) : String

@[deprecated String.Slice.trimAscii (since := "2025-11-20")]

def String.Slice.trim (s : Slice) : Slice

@[export lean_string_trim]

def String.Internal.trimImpl (s : String) : String

@[inline]

def String.Pos.Raw.nextWhile (s : String) (p : Char → Bool) (i : Raw) : Raw

Repeatedly increments a position in a string, as if by String.Pos.Raw.next, while the predicate p returns true for the character at the position. Stops incrementing at the end of the string or when p returns false for the current character.

Examples:

• let s := " a "; ((0 : Pos.Raw).nextWhile s Char.isWhitespace).get s = 'a'

• let s := "a "; ((0 : Pos.Raw).nextWhile s Char.isWhitespace).get s = 'a'

• let s := "ba "; (Pos.Raw.nextWhile s Char.isWhitespace 0).get s = 'b'

@[reducible, inline, deprecated String.Pos.Raw.nextWhile (since := "2025-10-10")]

abbrev String.nextWhile (s : String) (p : Char → Bool) (i : Pos.Raw) : Pos.Raw

@[export lean_string_nextwhile]

def String.Internal.nextWhileImpl (s : String) (p : Char → Bool) (i : Pos.Raw) : Pos.Raw

@[inline]

def String.Pos.Raw.nextUntil (s : String) (p : Char → Bool) (i : Raw) : Raw

Repeatedly increments a position in a string, as if by String.Pos.Raw.next, while the predicate p returns false for the character at the position. Stops incrementing at the end of the string or when p returns true for the current character.

Examples:

• let s := " a "; (Pos.Raw.nextUntil s Char.isWhitespace 0).get s = ' '

• let s := " a "; (Pos.Raw.nextUntil s Char.isAlpha 0).get s = 'a'

• let s := "a "; (Pos.Raw.nextUntil s Char.isWhitespace 0).get s = ' '

@[deprecated String.Pos.Raw.nextUntil (since := "2025-10-10")]

def String.nextUntil (s : String) (p : Char → Bool) (i : Pos.Raw) : Pos.Raw

def String.dropPrefix? {ρ : Type} (s : String) (pat : ρ) [Slice.Pattern.ForwardPattern pat] : Option Slice

If pat matches a prefix of s, returns the remainder. Returns none otherwise.

Use String.dropPrefix to return the slice unchanged when pat does not match a prefix.

This is a cheap operation because it does not allocate a new string to hold the result. To convert the result into a string, use String.Slice.copy.

This function is generic over all currently supported patterns.

Examples:

• "red green blue".dropPrefix? "red " == some "green blue".toSlice

• "red green blue".dropPrefix? "reed " == none

• "red green blue".dropPrefix? 'r' == some "ed green blue".toSlice

• "red green blue".dropPrefix? Char.isLower == some "ed green blue".toSlice

def String.dropSuffix? {ρ : Type} (s : String) (pat : ρ) [Slice.Pattern.BackwardPattern pat] : Option Slice

If pat matches a suffix of s, returns the remainder. Returns none otherwise.

Use String.dropSuffix to return the slice unchanged when pat does not match a suffix.

This is a cheap operation because it does not allocate a new string to hold the result. To convert the result into a string, use String.Slice.copy.

This function is generic over all currently supported patterns.

Examples:

• "red green blue".dropSuffix? " blue" == some "red green".toSlice

• "red green blue".dropSuffix? "bluu " == none

• "red green blue".dropSuffix? 'e' == some "red green blu".toSlice

• "red green blue".dropSuffix? Char.isLower == some "red green blu".toSlice

def String.dropPrefix {ρ : Type} (s : String) (pat : ρ) [Slice.Pattern.ForwardPattern pat] : Slice

If pat matches a prefix of s, returns the remainder. Returns s unmodified otherwise.

Use String.dropPrefix? to return none when pat does not match a prefix.

This is a cheap operation because it does not allocate a new string to hold the result. To convert the result into a string, use String.Slice.copy.

This function is generic over all currently supported patterns.

Examples:

• "red green blue".dropPrefix "red " == "green blue".toSlice

• "red green blue".dropPrefix "reed " == "red green blue".toSlice

• "red green blue".dropPrefix 'r' == "ed green blue".toSlice

• "red green blue".dropPrefix Char.isLower == "ed green blue".toSlice

@[deprecated String.dropPrefix (since := "2025-11-17")]

def String.stripPrefix (s pre : String) : String

@[deprecated String.Slice.dropPrefix (since := "2025-11-20")]

def String.Slice.stripPrefix (s pre : Slice) : Slice

def String.dropSuffix {ρ : Type} (s : String) (pat : ρ) [Slice.Pattern.BackwardPattern pat] : Slice

If pat matches a suffix of s, returns the remainder. Returns s unmodified otherwise.

Use String.dropSuffix? to return none when pat does not match a prefix.

This is a cheap operation because it does not allocate a new string to hold the result. To convert the result into a string, use String.Slice.copy.

This function is generic over all currently supported patterns.

Examples:

• "red green blue".dropSuffix " blue" == "red green".toSlice

• "red green blue".dropSuffix "bluu " == "red green blue".toSlice

• "red green blue".dropSuffix 'e' == "red green blu".toSlice

• "red green blue".dropSuffix Char.isLower == "red green blu".toSlice

@[deprecated String.dropSuffix (since := "2025-11-17")]

def String.stripSuffix (s suff : String) : String

@[deprecated String.Slice.dropSuffix (since := "2025-11-20")]

def String.Slice.stripSuffix (s suff : Slice) : Slice