@[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.toList.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.toList.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.toList.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.toList.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.all {ρ : Type} (s : String) (pat : ρ) [Slice.Pattern.ForwardPattern pat] : Bool

Checks whether a string only consists of matches of the pattern pat.

Short-circuits at the first pattern mis-match.

This function is generic over all currently supported patterns.

Examples:

• "brown".all Char.isLower = true

• "brown and orange".all Char.isLower = false

• "aaaaaa".all 'a' = true

• "aaaaaa".all "aa" = true

• "aaaaaaa".all "aa" = false

Equations

• s.all pat = s.toSlice.all pat

@[inline]

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

Checks whether a string only consists of matches of the pattern pat, starting from the back of the string.

Short-circuits at the first pattern mis-match.

This function is generic over all currently supported patterns.

For many types of patterns, this function can be expected to return the same result as String.all. If mismatches are expected to occur close to the end of the string, this function might be more efficient.

For some types of patterns, this function will return a different result than String.all. Consider, for example, a pattern that matches the longest string at the given position that matches the regular expression "a|aa|ab". Then, given the input string "aab", performing String.all will greedily match the prefix "aa" and then get stuck on the remainder "b", causing it to return false. On the other hand, String.revAll will match the suffix "ab" and then match the remainder "a", so it will return true.

Examples:

• "brown".revAll Char.isLower = true

• "brown and orange".revAll Char.isLower = false

• "aaaaaa".revAll 'a' = true

• "aaaaaa".revAll "aa" = true

• "aaaaaaa".revAll "aa" = false

Equations

• s.revAll pat = s.toSlice.revAll 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