The Substring type

This file contains API for Substring type, which is a legacy API that will be replaced by the safer variant String.Slice.

@[inline]

def Substring.Raw.isEmpty (ss : Raw) : Bool

Checks whether a substring is empty.

A substring is empty if its start and end positions are the same.

Equations

• ss.isEmpty = (ss.bsize == 0)

@[export lean_substring_isempty]

def Substring.Raw.Internal.isEmptyImpl (ss : Raw) : Bool

Equations

• Substring.Raw.Internal.isEmptyImpl ss = ss.isEmpty

@[inline]

def Substring.Raw.toString : Raw → String

Copies the region of the underlying string pointed to by a substring into a fresh string.

Equations

• { str := s, startPos := b, stopPos := e }.toString = String.Pos.Raw.extract s b e

@[export lean_substring_tostring]

def Substring.Raw.Internal.toStringImpl : Raw → String

Equations

• Substring.Raw.Internal.toStringImpl = Substring.Raw.toString

@[inline]

def Substring.Raw.get : Raw → String.Pos.Raw → Char

Returns the character at the given position in the substring.

The position is relative to the substring, rather than the underlying string, and no bounds checking is performed with respect to the substring's end position. If the relative position is not a valid position in the underlying string, the fallback value (default : Char), which is 'A', is returned. Does not panic.

Equations

• { str := s, startPos := b, stopPos := stopPos }.get x✝ = String.Pos.Raw.get s (x✝.offsetBy b)

@[export lean_substring_get]

def Substring.Raw.Internal.getImpl : Raw → String.Pos.Raw → Char

Equations

• Substring.Raw.Internal.getImpl = Substring.Raw.get

@[inline]

def Substring.Raw.next : Raw → String.Pos.Raw → String.Pos.Raw

Returns the next position in a substring after the given position. If the position is at the end of the substring, it is returned unmodified.

Both the input position and the returned position are interpreted relative to the substring's start position, not the underlying string.

Equations

• { str := s, startPos := b, stopPos := stopPos }.next x✝ = if x✝.offsetBy b = stopPos then x✝ else { byteIdx := (String.Pos.Raw.next s (x✝.offsetBy b)).byteIdx - b.byteIdx }

theorem Substring.Raw.lt_next (s : Raw) (i : String.Pos.Raw) (h : i.byteIdx < s.bsize) : i.byteIdx < (s.next i).byteIdx

@[inline]

def Substring.Raw.prev : Raw → String.Pos.Raw → String.Pos.Raw

Returns the previous position in a substring, just prior to the given position. If the position is at the beginning of the substring, it is returned unmodified.

Both the input position and the returned position are interpreted relative to the substring's start position, not the underlying string.

Equations

• { str := s, startPos := b, stopPos := stopPos }.prev x✝ = if x✝.offsetBy b = b then x✝ else { byteIdx := (String.Pos.Raw.prev s (x✝.offsetBy b)).byteIdx - b.byteIdx }

@[export lean_substring_prev]

def Substring.Raw.Internal.prevImpl : Raw → String.Pos.Raw → String.Pos.Raw

Equations

• Substring.Raw.Internal.prevImpl = Substring.Raw.prev

def Substring.Raw.nextn : Raw → Nat → String.Pos.Raw → String.Pos.Raw

Returns the position that's the specified number of characters forward from the given position in a substring. If the end position of the substring is reached, it is returned.

Both the input position and the returned position are interpreted relative to the substring's start position, not the underlying string.

Equations

• x✝¹.nextn 0 x✝ = x✝
• x✝¹.nextn i.succ x✝ = x✝¹.nextn i (x✝¹.next x✝)

def Substring.Raw.prevn : Raw → Nat → String.Pos.Raw → String.Pos.Raw

Returns the position that's the specified number of characters prior to the given position in a substring. If the start position of the substring is reached, it is returned.

Both the input position and the returned position are interpreted relative to the substring's start position, not the underlying string.

Equations

• x✝¹.prevn 0 x✝ = x✝
• x✝¹.prevn i.succ x✝ = x✝¹.prevn i (x✝¹.prev x✝)

@[inline]

def Substring.Raw.front (s : Raw) : Char

Returns the first character in the substring.

If the substring is empty, but the substring's start position is a valid position in the underlying string, then the character at the start position is returned. If the substring's start position is not a valid position in the string, the fallback value (default : Char), which is 'A', is returned. Does not panic.

Equations

• s.front = s.get 0

@[export lean_substring_front]

def Substring.Raw.Internal.frontImpl : Raw → Char

Equations

• Substring.Raw.Internal.frontImpl = Substring.Raw.front

@[inline]

def Substring.Raw.posOf (s : Raw) (c : Char) : String.Pos.Raw

Returns the substring-relative position of the first occurrence of c in s, or s.bsize if c doesn't occur.

Equations

• { str := s_1, startPos := b, stopPos := e }.posOf c = { byteIdx := (s_1.posOfAux c e b).byteIdx - b.byteIdx }

@[inline]

def Substring.Raw.drop : Raw → Nat → Raw

Removes the specified number of characters (Unicode code points) from the beginning of a substring by advancing its start position.

If the substring's end position is reached, the start position is not advanced past it.

Equations

• { str := s, startPos := b, stopPos := e }.drop x✝ = { str := s, startPos := ({ str := s, startPos := b, stopPos := e }.nextn x✝ 0).offsetBy b, stopPos := e }

@[export lean_substring_drop]

def Substring.Raw.Internal.dropImpl : Raw → Nat → Raw

Equations

• Substring.Raw.Internal.dropImpl = Substring.Raw.drop

@[inline]

def Substring.Raw.dropRight : Raw → Nat → Raw

Removes the specified number of characters (Unicode code points) from the end of a substring by moving its end position towards its start position.

If the substring's start position is reached, the end position is not retracted past it.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Substring.Raw.take : Raw → Nat → Raw

Retains only the specified number of characters (Unicode code points) at the beginning of a substring, by moving its end position towards its start position.

If the substring's start position is reached, the end position is not retracted past it.

Equations

• { str := s, startPos := b, stopPos := e }.take x✝ = { str := s, startPos := b, stopPos := ({ str := s, startPos := b, stopPos := e }.nextn x✝ 0).offsetBy b }

@[inline]

def Substring.Raw.takeRight : Raw → Nat → Raw

Retains only the specified number of characters (Unicode code points) at the end of a substring, by moving its start position towards its end position.

If the substring's end position is reached, the start position is not advanced past it.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Substring.Raw.atEnd : Raw → String.Pos.Raw → Bool

Checks whether a position in a substring is precisely equal to its ending position.

The position is understood relative to the substring's starting position, rather than the underlying string's starting position.

Equations

• { str := s, startPos := b, stopPos := stopPos }.atEnd x✝ = (x✝.offsetBy b == stopPos)

@[inline]

def Substring.Raw.extract : Raw → String.Pos.Raw → String.Pos.Raw → Raw

Returns the region of the substring delimited by the provided start and stop positions, as a substring. The positions are interpreted with respect to the substring's start position, rather than the underlying string.

If the resulting substring is empty, then the resulting substring is a substring of the empty string "". Otherwise, the underlying string is that of the input substring with the beginning and end positions adjusted.

Equations

• One or more equations did not get rendered due to their size.

@[export lean_substring_extract]

def Substring.Raw.Internal.extractImpl : Raw → String.Pos.Raw → String.Pos.Raw → Raw

Equations

• Substring.Raw.Internal.extractImpl = Substring.Raw.extract

def Substring.Raw.splitOn (s : Raw) (sep : String := " ") : List Raw

Splits a substring s on occurrences of the separator string sep. The default separator is " ".

When sep is empty, the result is [s]. When sep occurs in overlapping patterns, the first match is taken. There will always be exactly n+1 elements in the returned list if there were n non-overlapping matches of sep in the string. The separators are not included in the returned substrings, which are all substrings of s's string.

Equations

• s.splitOn sep = if (sep == "") = true then [s] else Substring.Raw.splitOn.loop✝ s sep 0 0 0 []

@[inline]

def Substring.Raw.foldl {α : Type u} (f : α → Char → α) (init : α) (s : Raw) : α

Folds a function over a substring from the left, accumulating a value starting with init. The accumulated value is combined with each character in order, using f.

Equations

• Substring.Raw.foldl f init { str := s_1, startPos := b, stopPos := e } = String.foldlAux f s_1 e b init

@[inline]

def Substring.Raw.foldr {α : Type u} (f : Char → α → α) (init : α) (s : Raw) : α

Folds a function over a substring from the right, accumulating a value starting with init. The accumulated value is combined with each character in reverse order, using f.

Equations

• Substring.Raw.foldr f init { str := s_1, startPos := b, stopPos := e } = String.foldrAux f init s_1 e b

@[inline]

def Substring.Raw.any (s : Raw) (p : Char → Bool) : Bool

Checks whether the Boolean predicate p returns true for any character in a substring.

Short-circuits at the first character for which p returns true.

Equations

• { str := s_1, startPos := b, stopPos := e }.any p = s_1.anyAux e p b

@[inline]

def Substring.Raw.all (s : Raw) (p : Char → Bool) : Bool

Checks whether the Boolean predicate p returns true for every character in a substring.

Short-circuits at the first character for which p returns false.

Equations

• s.all p = !s.any fun (c : Char) => !p c

@[export lean_substring_all]

def Substring.Raw.Internal.allImpl (s : Raw) (p : Char → Bool) : Bool

Equations

• Substring.Raw.Internal.allImpl s p = s.all p

@[inline]

def Substring.Raw.contains (s : Raw) (c : Char) : Bool

Checks whether a substring contains the specified character.

Equations

• s.contains c = s.any fun (a : Char) => a == c

@[irreducible, specialize #[]]

def Substring.Raw.takeWhileAux (s : String) (stopPos : String.Pos.Raw) (p : Char → Bool) (i : String.Pos.Raw) : String.Pos.Raw

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Substring.Raw.takeWhile : Raw → (Char → Bool) → Raw

Retains only the longest prefix of a substring in which a Boolean predicate returns true for all characters by moving the substring's end position towards its start position.

Equations

• { str := s, startPos := b, stopPos := e }.takeWhile x✝ = { str := s, startPos := b, stopPos := Substring.Raw.takeWhileAux s e x✝ b }

@[export lean_substring_takewhile]

def Substring.Raw.Internal.takeWhileImpl : Raw → (Char → Bool) → Raw

Equations

• Substring.Raw.Internal.takeWhileImpl = Substring.Raw.takeWhile

@[inline]

def Substring.Raw.dropWhile : Raw → (Char → Bool) → Raw

Removes the longest prefix of a substring in which a Boolean predicate returns true for all characters by moving the substring's start position. The start position is moved to the position of the first character for which the predicate returns false, or to the substring's end position if the predicate always returns true.

Equations

• { str := s, startPos := b, stopPos := e }.dropWhile x✝ = { str := s, startPos := Substring.Raw.takeWhileAux s e x✝ b, stopPos := e }

@[irreducible, specialize #[]]

def Substring.Raw.takeRightWhileAux (s : String) (begPos : String.Pos.Raw) (p : Char → Bool) (i : String.Pos.Raw) : String.Pos.Raw

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Substring.Raw.takeRightWhile : Raw → (Char → Bool) → Raw

Retains only the longest suffix of a substring in which a Boolean predicate returns true for all characters by moving the substring's start position towards its end position.

Equations

• { str := s, startPos := b, stopPos := e }.takeRightWhile x✝ = { str := s, startPos := Substring.Raw.takeRightWhileAux s b x✝ e, stopPos := e }

@[inline]

def Substring.Raw.dropRightWhile : Raw → (Char → Bool) → Raw

Removes the longest suffix of a substring in which a Boolean predicate returns true for all characters by moving the substring's end position. The end position is moved just after the position of the last character for which the predicate returns false, or to the substring's start position if the predicate always returns true.

Equations

• { str := s, startPos := b, stopPos := e }.dropRightWhile x✝ = { str := s, startPos := b, stopPos := Substring.Raw.takeRightWhileAux s b x✝ e }

@[inline]

def Substring.Raw.trimLeft (s : Raw) : Raw

Removes leading whitespace from a substring by moving its start position to the first non-whitespace character, or to its end position if there is no non-whitespace character.

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

Equations

• s.trimLeft = s.dropWhile Char.isWhitespace

@[inline]

def Substring.Raw.trimRight (s : Raw) : Raw

Removes trailing whitespace from a substring by moving its end position to the last non-whitespace character, or to its start position if there is no non-whitespace character.

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

Equations

• s.trimRight = s.dropRightWhile Char.isWhitespace

@[inline]

def Substring.Raw.trim : Raw → Raw

Removes leading and trailing whitespace from a substring by first moving its start position to the first non-whitespace character, and then moving its end position to the last non-whitespace character.

If the substring consists only of whitespace, then the resulting substring's start position is moved to its end position.

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

Examples:

• " red green blue ".toRawSubstring.trim.toString = "red green blue"
• " red green blue ".toRawSubstring.trim.startPos = ⟨1⟩
• " red green blue ".toRawSubstring.trim.stopPos = ⟨15⟩
• " ".toRawSubstring.trim.startPos = ⟨5⟩

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Substring.Raw.isNat (s : Raw) : Bool

Checks whether the substring can be interpreted as the decimal representation of a natural number.

A substring can be interpreted as a decimal natural number if it is not empty and all the characters in it are digits.

Use Substring.toNat? to convert such a substring to a natural number.

Equations

• s.isNat = (!s.isEmpty && s.all fun (c : Char) => c.isDigit)

def Substring.Raw.toNat? (s : Raw) : Option Nat

Checks whether the substring can be interpreted as the decimal representation of a natural number, returning the number if it can.

A substring can be interpreted as a decimal natural number if it is not empty and all the characters in it are digits.

Use Substring.isNat to check whether the substring is such a substring.

Equations

• s.toNat? = if s.isNat = true then some (Substring.Raw.foldl (fun (n : Nat) (c : Char) => n * 10 + (c.toNat - '0'.toNat)) 0 s) else none

def Substring.Raw.repair : Raw → Raw

Given a Substring, returns another one which has valid endpoints and represents the same substring according to Substring.toString. (Note, the substring may still be inverted, i.e. beginning greater than end.)

Equations

• One or more equations did not get rendered due to their size.

def Substring.Raw.beq (ss1 ss2 : Raw) : Bool

Checks whether two substrings represent equal strings. Usually accessed via the == operator.

Two substrings do not need to have the same underlying string or the same start and end positions; instead, they are equal if they contain the same sequence of characters.

Equations

• ss1.beq ss2 = (ss1.repair.bsize == ss2.repair.bsize && String.Pos.Raw.substrEq ss1.repair.str ss1.repair.startPos ss2.repair.str ss2.repair.startPos ss1.repair.bsize)

@[export lean_substring_beq]

def Substring.Raw.Internal.beqImpl (ss1 ss2 : Raw) : Bool

Equations

• Substring.Raw.Internal.beqImpl ss1 ss2 = ss1.beq ss2

instance Substring.Raw.hasBeq : BEq Raw

Equations

• Substring.Raw.hasBeq = { beq := Substring.Raw.beq }

def Substring.Raw.sameAs (ss1 ss2 : Raw) : Bool

Checks whether two substrings have the same position and content.

The two substrings do not need to have the same underlying string for this check to succeed.

Equations

• ss1.sameAs ss2 = (ss1.startPos == ss2.startPos && ss1 == ss2)

def Substring.Raw.commonPrefix (s t : Raw) : Raw

Returns the longest common prefix of two substrings.

The returned substring uses the same underlying string as s.

Equations

• s.commonPrefix t = { str := s.str, startPos := s.startPos, stopPos := Substring.Raw.commonPrefix.loop✝ s t s.startPos t.startPos }

def Substring.Raw.commonSuffix (s t : Raw) : Raw

Returns the longest common suffix of two substrings.

The returned substring uses the same underlying string as s.

Equations

• s.commonSuffix t = { str := s.str, startPos := Substring.Raw.commonSuffix.loop✝ s t s.stopPos t.stopPos, stopPos := s.stopPos }

def Substring.Raw.dropPrefix? (s pre : Raw) : Option Raw

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

The substring pre is a prefix of s if there exists a t : Substring such that s.toString = pre.toString ++ t.toString. If so, the result is the substring of s without the prefix.

Equations

• s.dropPrefix? pre = if (s.commonPrefix pre).bsize = pre.bsize then some { str := s.str, startPos := (s.commonPrefix pre).stopPos, stopPos := s.stopPos } else none

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

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

The substring suff is a suffix of s if there exists a t : Substring such that s.toString = t.toString ++ suff.toString. If so, the result the substring of s without the suffix.

Equations

• s.dropSuffix? suff = if (s.commonSuffix suff).bsize = suff.bsize then some { str := s.str, startPos := s.startPos, stopPos := (s.commonSuffix suff).startPos } else none

@[simp]

theorem Substring.Raw.prev_zero (s : Raw) : s.prev 0 = 0

@[simp]

theorem Substring.Raw.prevn_zero (s : Raw) (n : Nat) : s.prevn n 0 = 0

@[reducible, inline, deprecated Substring.Raw (since := "2025-11-16")]

abbrev Substring : Type

Equations

• Substring = Substring.Raw

@[reducible, inline, deprecated Substring.Raw.bsize (since := "2025-11-16")]

abbrev Substring.bsize : Raw → Nat

Equations

• Substring.bsize = Substring.Raw.bsize

@[reducible, inline, deprecated Substring.Raw.toString (since := "2025-11-16")]

abbrev Substring.toString : Raw → String

Equations

• Substring.toString = Substring.Raw.toString

@[reducible, inline, deprecated Substring.Raw.isEmpty (since := "2025-11-16")]

abbrev Substring.isEmpty (ss : Raw) : Bool

Equations

• Substring.isEmpty = Substring.Raw.isEmpty

@[reducible, inline, deprecated Substring.Raw.next (since := "2025-11-16")]

abbrev Substring.next : Raw → String.Pos.Raw → String.Pos.Raw

Equations

• Substring.next = Substring.Raw.next

@[reducible, inline, deprecated Substring.Raw.prev (since := "2025-11-16")]

abbrev Substring.prev : Raw → String.Pos.Raw → String.Pos.Raw

Equations

• Substring.prev = Substring.Raw.prev

@[reducible, inline, deprecated Substring.Raw.atEnd (since := "2025-11-16")]

abbrev Substring.atEnd : Raw → String.Pos.Raw → Bool

Equations

• Substring.atEnd = Substring.Raw.atEnd

@[reducible, inline, deprecated Substring.Raw.beq (since := "2025-11-16")]

abbrev Substring.beq (ss1 ss2 : Raw) : Bool

Equations

• Substring.beq = Substring.Raw.beq