@[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

Equations

• s.drop n = s.toSlice.drop n

@[export lean_string_drop]

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

Equations

• String.Internal.dropImpl s n = (s.drop n).copy

@[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

Equations

• s.dropEnd n = s.toSlice.dropEnd n

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

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

Equations

• s.dropRight n = (s.dropEnd n).copy

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

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

Equations

• s.dropRight n = s.dropEnd n

@[export lean_string_dropright]

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

Equations

• String.Internal.dropRightImpl s n = (s.dropEnd n).copy

@[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

Equations

• s.take n = s.toSlice.take n

@[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

Equations

• s.takeEnd n = s.toSlice.takeEnd n

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

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

Equations

• s.takeRight n = (s.takeEnd n).toString

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

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

Equations

• s.takeRight n = s.takeEnd n

@[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

Equations

• s.takeWhile pat = s.toSlice.takeWhile pat

@[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

Equations

• s.dropWhile pat = s.toSlice.dropWhile pat

@[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

Equations

• s.takeEndWhile pat = s.toSlice.takeEndWhile pat

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

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

Equations

• s.takeRightWhile p = (s.takeEndWhile p).toString

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

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

Equations

• s.takeRightWhile p = s.takeEndWhile p

@[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

Equations

• s.dropEndWhile pat = s.toSlice.dropEndWhile pat

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

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

Equations

• s.dropRightWhile p = (s.dropEndWhile p).toString

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

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

Equations

• s.dropRightWhile p = s.dropEndWhile p

@[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.

Equations

• s.skipPrefix? pat = Option.map String.Pos.ofToSlice (s.toSlice.skipPrefix? pat)

@[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).

Equations

• s.skipPrefixWhile pat = String.Pos.ofToSlice (s.toSlice.skipPrefixWhile pat)

@[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.

Equations

• pos.skip? pat = Option.map String.Pos.ofToSlice (pos.toSlice.skip? pat)

@[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.

Equations

• pos.skipWhile pat = String.Pos.ofToSlice (pos.toSlice.skipWhile pat)

@[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

Equations

• s.startsWith pat = s.toSlice.startsWith pat

@[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

Equations

• p.isPrefixOf s = s.startsWith p

@[export lean_string_isprefixof]

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

Equations

• String.Internal.isPrefixOfImpl p s = p.isPrefixOf s

@[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

Equations

• s.endsWith pat = s.toSlice.endsWith pat

@[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.

Equations

• s.skipSuffix? pat = Option.map String.Pos.ofToSlice (s.toSlice.skipSuffix? pat)

@[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).

Equations

• s.skipSuffixWhile pat = String.Pos.ofToSlice (s.toSlice.skipSuffixWhile pat)

@[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.

Equations

• pos.revSkip? pat = Option.map String.Pos.ofToSlice (pos.toSlice.revSkip? pat)

@[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.

Equations

• pos.revSkipWhile pat = String.Pos.ofToSlice (pos.toSlice.revSkipWhile pat)

@[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

Equations

• s.trimAsciiEnd = s.toSlice.trimAsciiEnd

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

def String.trimRight (s : String) : String

Equations

• s.trimRight = s.trimAsciiEnd.copy

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

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

Equations

• s.trimRight = s.trimAsciiEnd

@[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

Equations

• s.trimAsciiStart = s.toSlice.trimAsciiStart

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

def String.trimLeft (s : String) : String

Equations

• s.trimLeft = s.trimAsciiStart.copy

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

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

Equations

• s.trimLeft = s.trimAsciiStart

@[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

Equations

• s.trimAscii = s.toSlice.trimAscii

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

def String.trim (s : String) : String

Equations

• s.trim = s.trimAscii.copy

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

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

Equations

• s.trim = s.trimAscii

@[export lean_string_trim]

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

Equations

• String.Internal.trimImpl s = s.trimAscii.copy

@[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'

Equations

• String.Pos.Raw.nextWhile s p i = Substring.Raw.takeWhileAux s s.rawEndPos p i

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

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

Equations

• s.nextWhile p i = String.Pos.Raw.nextWhile s p i

@[export lean_string_nextwhile]

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

Equations

• String.Internal.nextWhileImpl s p i = String.Pos.Raw.nextWhile s p i

@[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 = ' '

Equations

• String.Pos.Raw.nextUntil s p i = String.Pos.Raw.nextWhile s (fun (c : Char) => !p c) i

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

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

Equations

• s.nextUntil p i = String.Pos.Raw.nextUntil s p i

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

Equations

• s.dropPrefix? pat = s.toSlice.dropPrefix? pat

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

Equations

• s.dropSuffix? pat = s.toSlice.dropSuffix? pat

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

Equations

• s.dropPrefix pat = s.toSlice.dropPrefix pat

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

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

Equations

• s.stripPrefix pre = (s.dropPrefix pre).toString

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

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

Equations

• s.stripPrefix pre = s.dropPrefix pre

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

Equations

• s.dropSuffix pat = s.toSlice.dropSuffix pat

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

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

Equations

• s.stripSuffix suff = (s.dropSuffix suff).toString

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

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

Equations

• s.stripSuffix suff = s.dropSuffix suff