String.take and variants

This file contains the implementations of String.take and its variants. Currently, they are implemented in terms of Substring; soon, they will be implemented in terms of String.Slice instead.

@[inline]

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

Removes the specified number of characters (Unicode code points) from the start of the string.

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

Examples:

• "red green blue".drop 4 = "green blue"
• "red green blue".drop 10 = "blue"
• "red green blue".drop 50 = ""

Equations

• s.drop n = (s.toRawSubstring.drop n).toString

@[export lean_string_drop]

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

Equations

• String.Internal.dropImpl s n = s.drop n

@[inline]

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

Removes the specified number of characters (Unicode code points) from the end of the string.

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

Examples:

• "red green blue".dropRight 5 = "red green"
• "red green blue".dropRight 11 = "red"
• "red green blue".dropRight 50 = ""

Equations

• s.dropRight n = (s.toRawSubstring.dropRight n).toString

@[export lean_string_dropright]

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

Equations

• String.Internal.dropRightImpl s n = s.dropRight n

@[inline]

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

Creates a new string that contains the first n characters (Unicode code points) of s.

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

Examples:

• "red green blue".take 3 = "red"
• "red green blue".take 1 = "r"
• "red green blue".take 0 = ""
• "red green blue".take 100 = "red green blue"

Equations

• s.take n = (s.toRawSubstring.take n).toString

@[inline]

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

Creates a new string that contains the last n characters (Unicode code points) of s.

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

Examples:

• "red green blue".takeRight 4 = "blue"
• "red green blue".takeRight 1 = "e"
• "red green blue".takeRight 0 = ""
• "red green blue".takeRight 100 = "red green blue"

Equations

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

@[inline]

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

Creates a new string that contains the longest prefix of s in which p returns true for all characters.

Examples:

• "red green blue".takeWhile (·.isLetter) = "red"
• "red green blue".takeWhile (· == 'r') = "r"
• "red green blue".takeWhile (· != 'n') = "red gree"
• "red green blue".takeWhile (fun _ => true) = "red green blue"

Equations

• s.takeWhile p = (s.toRawSubstring.takeWhile p).toString

@[inline]

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

Creates a new string by removing the longest prefix from s in which p returns true for all characters.

Examples:

• "red green blue".dropWhile (·.isLetter) = " green blue"
• "red green blue".dropWhile (· == 'r') = "ed green blue"
• "red green blue".dropWhile (· != 'n') = "n blue"
• "red green blue".dropWhile (fun _ => true) = ""

Equations

• s.dropWhile p = (s.toRawSubstring.dropWhile p).toString

@[inline]

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

Creates a new string that contains the longest suffix of s in which p returns true for all characters.

Examples:

• "red green blue".takeRightWhile (·.isLetter) = "blue"
• "red green blue".takeRightWhile (· == 'e') = "e"
• "red green blue".takeRightWhile (· != 'n') = " blue"
• "red green blue".takeRightWhile (fun _ => true) = "red green blue"

Equations

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

@[inline]

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

Creates a new string by removing the longest suffix from s in which p returns true for all characters.

Examples:

• "red green blue".dropRightWhile (·.isLetter) = "red green "
• "red green blue".dropRightWhile (· == 'e') = "red green blu"
• "red green blue".dropRightWhile (· != 'n') = "red green"
• "red green blue".dropRightWhile (fun _ => true) = ""

Equations

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

@[inline]

def String.startsWith (s pre : String) : Bool

Checks whether the first string (s) begins with the second (pre).

String.isPrefix 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".startsWith "red" = true

Equations

• s.startsWith pre = (s.toRawSubstring.take pre.length == pre.toRawSubstring)

@[inline]

def String.endsWith (s post : String) : Bool

Checks whether the first string (s) ends with the second (post).

Examples:

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

Equations

• s.endsWith post = (s.toRawSubstring.takeRight post.length == post.toRawSubstring)

@[inline]

def String.trimRight (s : String) : String

Removes trailing whitespace from a string.

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

Examples:

• "abc".trimRight = "abc"
• " abc".trimRight = " abc"
• "abc \t ".trimRight = "abc"
• " abc ".trimRight = " abc"
• "abc\ndef\n".trimRight = "abc\ndef"

Equations

• s.trimRight = s.toRawSubstring.trimRight.toString

@[inline]

def String.trimLeft (s : String) : String

Removes leading whitespace from a string.

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

Examples:

• "abc".trimLeft = "abc"
• " abc".trimLeft = " abc"
• "abc \t ".trimLeft = "abc \t "
• " abc ".trimLeft = "abc "
• "abc\ndef\n".trimLeft = "abc\ndef\n"

Equations

• s.trimLeft = s.toRawSubstring.trimLeft.toString

@[inline]

def String.trim (s : String) : String

Removes leading and trailing whitespace from a string.

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

Examples:

• "abc".trim = "abc"
• " abc".trim = "abc"
• "abc \t ".trim = "abc"
• " abc ".trim = "abc"
• "abc\ndef\n".trim = "abc\ndef"

Equations

• s.trim = s.toRawSubstring.trim.toString

@[export lean_string_trim]

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

Equations

• String.Internal.trimImpl s = s.trim

@[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.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 "; s.get (s.nextWhile Char.isWhitespace 0) = 'a'
• let s := "a "; s.get (s.nextWhile Char.isWhitespace 0) = 'a'
• let s := "ba "; s.get (s.nextWhile Char.isWhitespace 0) = '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.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 "; s.get (s.nextUntil Char.isWhitespace 0) = ' '
• let s := " a "; s.get (s.nextUntil Char.isLetter 0) = 'a'
• let s := "a "; s.get (s.nextUntil Char.isWhitespace 0) = ' '

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? (s pre : String) : Option Substring.Raw

If pre is a prefix of s, returns the remainder. Returns none otherwise.

The string pre is a prefix of s if there exists a t : String such that s = pre ++ t. If so, the result is some t.

Use String.stripPrefix to return the string unchanged when pre is not a prefix.

Examples:

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

Equations

• s.dropPrefix? pre = s.toRawSubstring.dropPrefix? pre.toRawSubstring

def String.dropSuffix? (s suff : String) : Option Substring.Raw

If suff is a suffix of s, returns the remainder. Returns none otherwise.

The string suff is a suffix of s if there exists a t : String such that s = t ++ suff. If so, the result is some t.

Use String.stripSuffix to return the string unchanged when suff is not a suffix.

Examples:

• "red green blue".dropSuffix? " blue" = some "red green"
• "red green blue".dropSuffix? " blu " = none
• "red green blue".dropSuffix? "" = some "red green blue"

Equations

• s.dropSuffix? suff = s.toRawSubstring.dropSuffix? suff.toRawSubstring

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

If pre is a prefix of s, returns the remainder. Returns s unmodified otherwise.

The string pre is a prefix of s if there exists a t : String such that s = pre ++ t. If so, the result is t. Otherwise, it is s.

Use String.dropPrefix? to return none when pre is not a prefix.

Examples:

• "red green blue".stripPrefix "red " = "green blue"
• "red green blue".stripPrefix "reed " = "red green blue"
• "red green blue".stripPrefix "" = "red green blue"

Equations

• s.stripPrefix pre = (Option.map Substring.Raw.toString (s.dropPrefix? pre)).getD s

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

If suff is a suffix of s, returns the remainder. Returns s unmodified otherwise.

The string suff is a suffix of s if there exists a t : String such that s = t ++ suff. If so, the result is t. Otherwise, it is s.

Use String.dropSuffix? to return none when suff is not a suffix.

Examples:

• "red green blue".stripSuffix " blue" = "red green"
• "red green blue".stripSuffix " blu " = "red green blue"
• "red green blue".stripSuffix "" = "red green blue"

Equations

• s.stripSuffix suff = (Option.map Substring.Raw.toString (s.dropSuffix? suff)).getD s