Strings represent Unicode text. Strings are specially supported by Lean:
They have a logical model that specifies their behavior in terms of lists of characters, which specifies the meaning of each operation on strings.
They have an optimized run-time representation in compiled code, as packed arrays of bytes that encode the string as UTF-8, and the Lean runtime specially optimizes string operations.
There is string literal syntax for writing strings.
The fact that strings are internally represented as UTF-8-encoded byte arrays is visible in the API:
There is no operation to project a particular character out of the string, as this would be a performance trap. Use a String.Iterator in a loop instead of a Nat.
Strings are indexed by String.Pos, which internally records byte counts rather than character counts, and thus takes constant time. Aside from 0, these should not be constructed directly, but rather updated using String.next and String.prev.
String : TypeA string is a sequence of Unicode code points.
At runtime, strings are represented by dynamic arrays
of bytes using the UTF-8 encoding. Both the size in bytes (String.utf8ByteSize) and in characters
(String.length) are cached and take constant time. Many operations on strings perform in-place
modifications when the reference to the string is unique.
String.mk
data : List Char
The logical model of strings in Lean is a structure that contains a single field, which is a list of characters. This is convenient when specifying and proving properties of string-processing functions at a low level.
Strings are represented as dynamic arrays of bytes, encoded in UTF-8. After the object header, a string contains:
The number of bytes that currently contain valid string data
The number of bytes presently allocated for the string
The length of the encoded string, which may be shorter than the byte count due to UTF-8 multi-byte characters
The actual character data in the string, null-terminated
Many string functions in the Lean runtime check whether they have exclusive access to their argument by consulting the reference count in the object header. If they do, and the string's capacity is sufficient, then the existing string can be mutated rather than allocating fresh memory. Otherwise, a new string must be allocated.
Despite the fact that they appear to be an ordinary constructor and projection, String.mk and String.data take time linear in the length of the string.
This is because they must implement the conversions between lists of characters and packed arrays of bytes, which must necessarily visit each character.
Lean has three kinds of string literals: ordinary string literals, interpolated string literals, and raw string literals.
String literals begin and end with a double-quote character ".
Between these characters, they may contain any other character, including newlines, which are included literally (with the caveat that all newlines in a Lean source file are interpreted as '\n', regardless of file encoding and platform).
Special characters that cannot otherwise be written in string literals may be escaped with a backslash, so "\"Quotes\"" is a string literal that begins and ends with double quotes.
The following forms of escape sequences are accepted:
\r, \n, \t, \\, \", \'
These escape sequences have the usual meaning, mapping to CR, LF, tab, backslash, double quote, and single quote, respectively.
\xNN
When NN is a sequence of two hexadecimal digits, this escape denotes the character whose Unicode code point is indicated by the two-digit hexadecimal code.
\uNNNN
When NN is a sequence of two hexadecimal digits, this escape denotes the character whose Unicode code point is indicated by the four-digit hexadecimal code.
String literals may contain gaps. A gap is indicated by an escaped newline, with no intervening characters between the escaping backslash and the newline. In this case, the string denoted by the literal is missing the newline and all leading whitespace from the next line. String gaps may not precede lines that contain only whitespace.
Here, str1 and str2 are the same string:
def str1 := "String with \
a gap"
def str2 := "String with a gap"
example : str1 = str2 := rfl
If the line following the gap is empty, the string is rejected:
def str3 := "String with \a gap"
The parser error is:
<example>:2:0-3:0: unexpected additional newline in string gap
Preceding a string literal with s! causes it to be processed as an interpolated string, in which regions of the string surrounded by { and } characters are parsed and interpreted as Lean expressions.
Interpolated strings are interpreted by appending the string that precedes the interpolation, the expression (with an added call to toString surrounding it), and the string that follows the interpolation.
For example:
example :
s!"1 + 1 = {1 + 1}\n" =
"1 + 1 = " ++ toString (1 + 1) ++ "\n" :=
rfl
Preceding a literal with m! causes the interpolation to result in an instance of MessageData, the compiler's internal data structure for messages to be shown to users.
In raw string literals, there are no escape sequences or gaps, and each character denotes itself exactly.
Raw string literals are preceded by r, followed by zero or more hash characters (#) and a double quote ".
The string literal is completed at a double quote that is followed by the same number of hash characters.
For example, they can be used to avoid the need to double-escape certain characters:
example : r"\t" = "\\t" := rfl
#eval r"Write backslash in a string using '\\\\'"
The #eval yields:
"Write backslash in a string using '\\\\\\\\'"
Including hash marks allows the strings to contain unescaped quotes:
example :
r#"This is "literally" quoted"# =
"This is \"literally\" quoted" :=
rfl
Adding sufficiently many hash marks allows any raw literal to be written literally:
example :
r##"This is r#"literally"# quoted"## =
"This is r#\"literally\"# quoted" :=
rfl
String.singleton (c : Char) : String
Returns a new string that contains only the character c.
Because strings are encoded in UTF-8, the resulting string may take multiple bytes.
Examples:
String.singleton 'L' = "L"
String.singleton ' ' = " "
String.singleton '"' = "\""
String.singleton 'π«' = "π«"
String.append : String β String β String
Appends two strings. Usually accessed via the ++ operator.
The internal implementation will perform destructive updates if the string is not shared.
Examples:
"abc".append "def" = "abcdef"
"abc" ++ "def" = "abcdef"
"" ++ "" = ""
String.join (l : List String) : String
Appends all the strings in a list of strings, in order.
Use String.intercalate to place a separator string between the strings in a list.
Examples:
String.join ["gr", "ee", "n"] = "green"
String.join ["b", "", "l", "", "ue"] = "red"
String.join [] = ""
String.intercalate (s : String) : List String β String
Appends the strings in a list of strings, placing the separator s between each pair.
Examples:
", ".intercalate ["red", "green", "blue"] = "red, green, blue"
" and ".intercalate ["tea", "coffee"] = "tea and coffee"
" | ".intercalate ["M", "", "N"] = "M | | N"
String.toList (s : String) : List Char
Converts a string to a list of characters.
Even though the logical model of strings is as a structure that wraps a list of characters, this operation takes time and space linear in the length of the string. At runtime, strings are represented as dynamic arrays of bytes.
Examples:
String.isNat (s : String) : Bool
Checks whether the string can be interpreted as the decimal representation of a natural number.
A string can be interpreted as a decimal natural number if it is not empty and all the characters in it are digits.
Use String.toNat? or String.toNat! to convert such a string to a natural number.
Examples:
String.toNat? (s : String) : Option Nat
Interprets a string as the decimal representation of a natural number, returning it. Returns none
if the string does not contain a decimal natural number.
A string can be interpreted as a decimal natural number if it is not empty and all the characters in it are digits.
Use String.isNat to check whether String.toNat? would return some. String.toNat! is an
alternative that panics instead of returning none when the string is not a natural number.
Examples:
String.toNat! (s : String) : Nat
Interprets a string as the decimal representation of a natural number, returning it. Panics if the string does not contain a decimal natural number.
A string can be interpreted as a decimal natural number if it is not empty and all the characters in it are digits.
Use String.isNat to check whether String.toNat! would return a value. String.toNat? is a safer
alternative that returns none instead of panicking when the string is not a natural number.
Examples:
String.isInt (s : String) : Bool
Checks whether the string can be interpreted as the decimal representation of an integer.
A string can be interpreted as a decimal integer if it is not empty, its first character is
'-' or a digit, and all subsequent characters are digits. Leading + characters are not allowed.
Use String.toInt? or String.toInt! to convert such a string to an integer.
Examples:
String.toInt? (s : String) : Option Int
Interprets a string as the decimal representation of an integer, returning it. Returns none if the
string does not contain a decimal integer.
A string can be interpreted as a decimal integer if it is not empty, its first character is either
'-' or a digit, and all remaining characters are digits.
Use String.isInt to check whether String.toInt? would return some. String.toInt! is an
alternative that panics instead of returning none when the string is not an integer.
Examples:
String.toInt! (s : String) : Int
Interprets a string as the decimal representation of an integer, returning it. Panics if the string does not contain a decimal integer.
A string can be interpreted as a decimal integer if it is not empty, its first character is '-' or
a digit, and all remaining characters are digits.
Use String.isInt to check whether String.toInt! would return a value. String.toInt? is a safer
alternative that returns none instead of panicking when the string is not an integer.
Examples:
String.toFormat (s : String) : Std.Format
Converts a string to a pretty-printer document, replacing newlines in the string with
Std.Format.line.
String.Pos : Type
A byte position in a String, according to its UTF-8 encoding.
Character positions (counting the Unicode code points rather than bytes) are represented by plain
Nats. Indexing a String by a String.Pos takes constant time, while character positions need to
be translated internally to byte positions, which takes linear time.
A byte position p is valid for a string s if 0 β€ p β€ s.endPos and p lies on a UTF-8
character boundary.
String.Pos.mk
byteIdx : Nat
Get the underlying byte index of a String.Pos
String.Pos.isValid (s : String) (p : String.Pos) : Bool
Returns true if p is a valid UTF-8 position in the string s.
This means that p β€ s.endPos and p lies on a UTF-8 character boundary. At runtime, this
operation takes constant time.
Examples:
String.Pos.isValid "abc" β¨0β© = true
String.Pos.isValid "abc" β¨1β© = true
String.Pos.isValid "abc" β¨3β© = true
String.Pos.isValid "abc" β¨4β© = false
String.Pos.isValid "π«(A)" β¨0β© = true
String.Pos.isValid "π«(A)" β¨1β© = false
String.Pos.isValid "π«(A)" β¨2β© = false
String.Pos.isValid "π«(A)" β¨3β© = false
String.Pos.isValid "π«(A)" β¨4β© = true
String.atEnd : String β String.Pos β Bool
Returns true if a specified byte position is greater than or equal to the position which points to
the end of a string. Otherwise, returns false.
Examples:
String.endPos (s : String) : String.Pos
String.next (s : String) (p : String.Pos) : String.Pos
Returns the next position in a string after position p. The result is unspecified if p is not a
valid position or if p = s.endPos.
A run-time bounds check is performed to determine whether p is at the end of the string. If a
bounds check has already been performed, use String.next' to avoid a repeated check.
Some examples where the result is unspecified:
"LββN".next β¨2β©, since 2 points into the middle of a multi-byte UTF-8 character
Examples:
String.next' (s : String) (p : String.Pos) (h : Β¬s.atEnd p = true) : String.Pos
Returns the next position in a string after position p. The result is unspecified if p is not a
valid position.
Requires evidence, h, that p is within bounds. No run-time bounds check is performed, as in
String.next.
A typical pattern combines String.next' with a dependent if-expression to avoid the overhead of
an additional bounds check. For example:
def next? (s: String) (p : String.Pos) : Option Char :=
if h : s.atEnd p then none else s.get (s.next' p h)
Example:
String.nextWhile (s : String) (p : Char β Bool) (i : String.Pos) : String.Pos
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'
String.nextUntil (s : String) (p : Char β Bool) (i : String.Pos) : String.Pos
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.isWhitespace 0) = ' '
String.prev : String β String.Pos β String.Pos
Returns the position in a string before a specified position, p. If p = β¨0β©, returns 0. If p
is not a valid position, the result is unspecified.
For example, "LββN".prev β¨3β© is unspecified, since byte 3 occurs in the middle of the multi-byte
character 'β'.
Examples:
String.Pos.min (pβ pβ : String.Pos) : String.Pos
Returns either pβ or pβ, whichever has the least byte index.
String.get (s : String) (p : String.Pos) : Char
Returns the character at position p of a string. If p is not a valid position, returns the
fallback value (default : Char), which is 'A', but does not panic.
This function is overridden with an efficient implementation in runtime code. See
String.utf8GetAux for the reference implementation.
Examples:
String.get? : String β String.Pos β Option Char
Returns the character at position p of a string. If p is not a valid position, returns none.
This function is overridden with an efficient implementation in runtime code. See
String.utf8GetAux? for the reference implementation.
Examples:
String.get! (s : String) (p : String.Pos) : Char
Returns the character at position p of a string. Panics if p is not a valid position.
See String.get? for a safer alternative.
This function is overridden with an efficient implementation in runtime code. See
String.utf8GetAux for the reference implementation.
Examples
"abc".get! β¨1β© = 'b'
String.get' (s : String) (p : String.Pos) (h : Β¬s.atEnd p = true) : Char
Returns the character at position p of a string. Returns (default : Char), which is 'A', if
p is not a valid position.
Requires evidence, h, that p is within bounds instead of performing a run-time bounds check as
in String.get.
A typical pattern combines get' with a dependent if-expression to avoid the overhead of an
additional bounds check. For example:
def getInBounds? (s : String) (p : String.Pos) : Option Char :=
if h : s.atEnd p then none else some (s.get' p h)
Even with evidence of Β¬ s.atEnd p, p may be invalid if a byte index points into the middle of a
multi-byte UTF-8 character. For example, "LββN".get' β¨2β© (by decide) = (default : Char).
Examples:
String.extract : String β String.Pos β String.Pos β String
Creates a new string that consists of the region of the input string delimited by the two positions.
The result is "" if the start position is greater than or equal to the end position or if the
start position is at the end of the string. If either position is invalid (that is, if either points
at the middle of a multi-byte UTF-8 character) then the result is unspecified.
Examples:
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:
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"
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:
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) = ""
String.dropPrefix? (s pre : String) : Option Substring
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"
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"
String.dropSuffix? (s suff : String) : Option Substring
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"
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"
String.removeLeadingSpaces (s : String) : String
Consistently de-indents the lines in a string, removing the same amount of leading whitespace from each line such that the least-indented line has no leading whitespace.
The number of leading whitespace characters to remove from each line is determined by counting the
number of leading space (' ') and tab ('\t') characters on lines after the first line that also
contain non-whitespace characters. No distinction is made between tab and space characters; both
count equally.
The least number of leading whitespace characters found is then removed from the beginning of each line. The first line's leading whitespace is not counted when determining how far to de-indent the string, but leading whitespace is removed from it.
Examples:
"Here:\n fun x =>\n x + 1".removeLeadingSpaces = "Here:\nfun x =>\n x + 1"
"Here:\n\t\tfun x =>\n\t \tx + 1".removeLeadingSpaces = "Here:\nfun x =>\n \tx + 1"
"Here:\n\t\tfun x =>\n \n\t \tx + 1".removeLeadingSpaces = "Here:\nfun x =>\n\n \tx + 1"
String.set : String β String.Pos β Char β String
Replaces the character at a specified position in a string with a new character. If the position is invalid, the string is returned unchanged.
If both the replacement character and the replaced character are 7-bit ASCII characters and the string is not shared, then it is updated in-place and not copied.
Examples:
String.modify (s : String) (i : String.Pos) (f : Char β Char) : String
Replaces the character at position p in the string s with the result of applying f to that
character. If p is an invalid position, the string is returned unchanged.
If both the replacement character and the replaced character are 7-bit ASCII characters and the string is not shared, then it is updated in-place and not copied.
Examples:
abc.modify β¨1β© Char.toUpper = "aBc"
abc.modify β¨3β© Char.toUpper = "abc"
String.posOf (s : String) (c : Char) : String.Pos
String.revPosOf (s : String) (c : Char) : Option String.Pos
String.offsetOfPos (s : String) (pos : String.Pos) : Nat
Returns the character index that corresponds to the provided position (i.e. UTF-8 byte index) in a string.
If the position is at the end of the string, then the string's length in characters is returned. If the position is invalid due to pointing at the middle of a UTF-8 byte sequence, then the character index of the next character after the position is returned.
Examples:
"LββN".offsetOfPos β¨0β© = 0
"LββN".offsetOfPos β¨1β© = 1
"LββN".offsetOfPos β¨2β© = 2
"LββN".offsetOfPos β¨4β© = 2
"LββN".offsetOfPos β¨5β© = 3
"LββN".offsetOfPos β¨50β© = 4
String.findLineStart (s : String) (pos : String.Pos) : String.Pos
Returns the position of the beginning of the line that contains the position pos.
Lines are ended by '\n', and the returned position is either 0 : String.Pos or immediately after
a '\n' character.
String.find (s : String) (p : Char β Bool) : String.Pos
Finds the position of the first character in a string for which the Boolean predicate p returns
true. If there is no such character in the string, then the end position of the string is
returned.
Examples:
"coffee tea water".find (Β·.isWhitespace) = β¨6β©
"tea".find (Β· == 'X') = β¨3β©
"".find (Β· == 'X') = β¨0β©
String.map (f : Char β Char) (s : String) : String
Applies the function f to every character in a string, returning a string that contains the
resulting characters.
Examples:
"abc123".map Char.toUpper = "ABC123"
"".map Char.toUpper = ""
String.foldl.{u} {Ξ± : Type u} (f : Ξ± β Char β Ξ±)
(init : Ξ±) (s : String) : Ξ±
Folds a function over a string from the left, accumulating a value starting with init. The
accumulated value is combined with each character in order, using f.
Examples:
String.foldr.{u} {Ξ± : Type u} (f : Char β Ξ± β Ξ±)
(init : Ξ±) (s : String) : Ξ±
Folds a function over a string from the right, accumulating a value starting with init. The
accumulated value is combined with each character in reverse order, using f.
Examples:
The LT String instance is defined by the lexicographic ordering on strings based on the LT Char instance.
Logically, this is modeled by the lexicographic ordering on the lists that model strings, so List.Lex defines the order.
It is decidable, and the decision procedure is overridden at runtime with efficient code that takes advantage of the run-time representation of strings.
String.le (a b : String) : Prop
Non-strict inequality on strings, typically used via the β€ operator.
a β€ b is defined to mean Β¬ b < a.
String.firstDiffPos (a b : String) : String.Pos
Returns the first position where the two strings differ.
If one string is a prefix of the other, then the returned position is the end position of the shorter string. If the strings are identical, then their end position is returned.
Examples:
"tea".firstDiffPos "ten" = β¨2β©
"tea".firstDiffPos "tea" = β¨3β©
"tea".firstDiffPos "teas" = β¨3β©
"teas".firstDiffPos "tea" = β¨3β©
String.substrEq (s1 : String) (pos1 : String.Pos) (s2 : String) (pos2 : String.Pos) (sz : Nat) : Bool
Checks whether substrings of two strings are equal. Substrings are indicated by their starting
positions and a size in UTF-8 bytes. Returns false if the indicated substring does not exist in
either string.
String.isPrefixOf (p s : String) : Bool
Checks whether the first string (p) is a prefix of the second (s).
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
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
String.split (s : String) (p : Char β Bool) : List String
Splits a string at each character for which p returns true.
The characters that satisfy p are not included in any of the resulting strings. If multiple
characters in a row satisfy p, then the resulting list will contain empty strings.
Examples:
"coffee tea water".split (Β·.isWhitespace) = ["coffee", "tea", "water"]
"coffee tea water".split (Β·.isWhitespace) = ["coffee", "", "tea", "", "water"]
"fun x =>\n x + 1\n".split (Β· == '\n') = ["fun x =>", " x + 1", ""]
String.splitOn (s : String) (sep : String := " ") : List String
Splits a string 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.
Examples:
String.pushn (s : String) (c : Char) (n : Nat) : String
Adds multiple repetitions of a character to the end of a string.
Returns s, with n repetitions of c at the end. Internally, the implementation repeatedly calls
String.push, so the string is modified in-place if there is a unique reference to it.
Examples:
String.capitalize (s : String) : String
Replaces the first character in s with the result of applying Char.toUpper to it. Returns the
empty string if the string is empty.
Char.toUpper has no effect on characters outside of the range 'a'β'z'.
Examples:
"orange".capitalize = "Orange"
"ORANGE".capitalize = "ORANGE"
"".capitalize = ""
String.decapitalize (s : String) : String
Replaces the first character in s with the result of applying Char.toLower to it. Returns the
empty string if the string is empty.
Char.toLower has no effect on characters outside of the range 'A'β'Z'.
Examples:
"Orange".decapitalize = "orange"
"ORANGE".decapitalize = "oRANGE"
"".decapitalize = ""
String.toUpper (s : String) : String
Replaces each character in s with the result of applying Char.toUpper to it.
Char.toUpper has no effect on characters outside of the range 'a'β'z'.
Examples:
String.toLower (s : String) : String
Replaces each character in s with the result of applying Char.toLower to it.
Char.toLower has no effect on characters outside of the range 'A'β'Z'.
Examples:
Fundamentally, a String.Iterator is a pair of a string and a valid position in the string.
Iterators provide functions for getting the current character (curr), replacing the current character (setCurr), checking whether the iterator can move to the left or the right (hasPrev and hasNext, respectively), and moving the iterator (prev and next, respectively).
Clients are responsible for checking whether they've reached the beginning or end of the string; otherwise, the iterator ensures that its position always points at a character.
String.Iterator : Type
An iterator over the characters (Unicode code points) in a String. Typically created by
String.iter.
String iterators pair a string with a valid byte index. This allows efficient character-by-character processing of strings while avoiding the need to manually ensure that byte indices are used with the correct strings.
An iterator is valid if the position i is valid for the string s, meaning 0 β€ i β€ s.endPos
and i lies on a UTF8 byte boundary. If i = s.endPos, the iterator is at the end of the string.
Most operations on iterators return unspecified values if the iterator is not valid. The functions
in the String.Iterator API rule out the creation of invalid iterators, with two exceptions:
Iterator.next iter is invalid if iter is already at the end of the string (iter.atEnd is
true), and
Iterator.forward iter n/Iterator.nextn iter n is invalid if n is strictly greater than the
number of remaining characters.
String.Iterator.mk
s : String
The string being iterated over.
i : String.Pos
The current UTF-8 byte position in the string s.
This position is not guaranteed to be valid for the string. If the position is not valid, then the
current character is (default : Char), similar to String.get on an invalid position.
String.mkIterator (s : String) : String.Iterator
Creates an iterator at the beginning of the string.
String.Iterator.curr : String.Iterator β Char
String.Iterator.hasNext : String.Iterator β Bool
Checks whether the iterator is at or before the string's last character.
String.Iterator.next : String.Iterator β String.Iterator
Moves the iterator's position forward by one character, unconditionally.
It is only valid to call this function if the iterator is not at the end of the string (i.e.
if Iterator.atEnd is false); otherwise, the resulting iterator will be invalid.
String.Iterator.forward : String.Iterator β Nat β String.Iterator
Moves the iterator's position forward by the specified number of characters.
The resulting iterator is only valid if the number of characters to skip is less than or equal to the number of characters left in the iterator.
String.Iterator.nextn : String.Iterator β Nat β String.Iterator
Moves the iterator's position forward by the specified number of characters.
The resulting iterator is only valid if the number of characters to skip is less than or equal to the number of characters left in the iterator.
String.Iterator.hasPrev : String.Iterator β Bool
Checks whether the iterator is after the beginning of the string.
String.Iterator.prev : String.Iterator β String.Iterator
Moves the iterator's position backward by one character, unconditionally.
The position is not changed if the iterator is at the beginning of the string.
String.Iterator.prevn : String.Iterator β Nat β String.Iterator
Moves the iterator's position back by the specified number of characters, stopping at the beginning of the string.
String.Iterator.atEnd : String.Iterator β Bool
Checks whether the iterator is past its string's last character.
String.Iterator.toEnd : String.Iterator β String.Iterator
Moves the iterator's position to the end of the string, just past the last character.
String.Iterator.setCurr : String.Iterator β Char β String.Iterator
Replaces the current character in the string.
Does nothing if the iterator is at the end of the string. If both the replacement character and the replaced character are 7-bit ASCII characters and the string is not shared, then it is updated in-place and not copied.
String.Iterator.extract : String.Iterator β String.Iterator β String
Extracts the substring between the positions of two iterators. The first iterator's position is the start of the substring, and the second iterator's position is the end.
Returns the empty string if the iterators are for different strings, or if the position of the first iterator is past the position of the second iterator.
String.Iterator.remainingToString : String.Iterator β String
The remaining characters in an iterator, as a string.
String.Iterator.remainingBytes : String.Iterator β Nat
The number of UTF-8 bytes remaining in the iterator.
String.Iterator.pos (self : String.Iterator) : String.Pos
The current UTF-8 byte position in the string s.
This position is not guaranteed to be valid for the string. If the position is not valid, then the
current character is (default : Char), similar to String.get on an invalid position.
String.toSubstring' (s : String) : Substring
Converts a String into a Substring that denotes the entire string.
This is a version of String.toSubstring that doesn't have an @[inline] annotation.
Substring : TypeA region or slice of some underlying string.
A substring contains an string together with the start and end byte positions of a region of interest. Actually extracting a substring requires copying and memory allocation, while many substrings of the same underlying string may exist with very little overhead, and they are more convenient than tracking the bounds by hand.
Using its constructor explicitly, it is possible to construct a Substring in which one or both of
the positions is invalid for the string. Many operations will return unexpected or confusing results
if the start and stop positions are not valid. Instead, it's better to use API functions that ensure
the validity of the positions in a substring to create and manipulate them.
Substring.mk
str : String
The underlying string.
startPos : String.Pos
The byte position of the start of the string slice.
stopPos : String.Pos
The byte position of the end of the string slice.
Substring.atEnd : Substring β String.Pos β 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.
Substring.posOf (s : Substring) (c : Char) : String.Pos
Returns the substring-relative position of the first occurrence of c in s, or s.bsize if c
doesn't occur.
Substring.next : Substring β String.Pos β String.Pos
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.
Substring.nextn : Substring β Nat β String.Pos β String.Pos
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.
Substring.prev : Substring β String.Pos β String.Pos
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.
Substring.prevn : Substring β Nat β String.Pos β String.Pos
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.
Substring.foldl.{u} {Ξ± : Type u}
(f : Ξ± β Char β Ξ±) (init : Ξ±)
(s : Substring) : Ξ±
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.
Substring.foldr.{u} {Ξ± : Type u}
(f : Char β Ξ± β Ξ±) (init : Ξ±)
(s : Substring) : Ξ±
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.
Substring.beq (ss1 ss2 : Substring) : 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.
Substring.commonPrefix (s t : Substring) : Substring
Returns the longest common prefix of two substrings.
The returned substring uses the same underlying string as s.
Substring.commonSuffix (s t : Substring) : Substring
Returns the longest common suffix of two substrings.
The returned substring uses the same underlying string as s.
Substring.get : Substring β String.Pos β 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.
Substring.contains (s : Substring) (c : Char) : Bool
Checks whether a substring contains the specified character.
Substring.front (s : Substring) : 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.
Substring.drop : Substring β Nat β Substring
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.
Substring.dropWhile : Substring β (Char β Bool) β Substring
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.
Substring.dropRight : Substring β Nat β Substring
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.
Substring.dropRightWhile : Substring β (Char β Bool) β Substring
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.
Substring.take : Substring β Nat β Substring
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.
Substring.takeWhile : Substring β (Char β Bool) β Substring
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.
Substring.takeRight : Substring β Nat β Substring
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.
Substring.takeRightWhile : Substring β (Char β Bool) β Substring
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.
Substring.extract : Substring β String.Pos β String.Pos β Substring
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.
Substring.trim : Substring β Substring
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 ".toSubstring.trim.toString = "red green blue"
" red green blue ".toSubstring.trim.startPos = β¨1β©
" red green blue ".toSubstring.trim.stopPos = β¨15β©
" ".toSubstring.trim.startPos = β¨5β©
Substring.trimLeft (s : Substring) : Substring
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.
Substring.trimRight (s : Substring) : Substring
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.
Substring.splitOn (s : Substring) (sep : String := " ") : List Substring
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.
Substring.toString : Substring β String
Copies the region of the underlying string pointed to by a substring into a fresh string.
Substring.isNat (s : Substring) : 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.
Substring.toNat? (s : Substring) : 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.
Substring.toIterator : Substring β String.Iterator
Returns an iterator into the underlying string, at the substring's starting position. The ending position is discarded, so the iterator alone cannot be used to determine whether its current position is within the original substring.
Substring.toName (s : Substring) : Lean.Name
Converts a substring to the Lean compiler's representation of names. The resulting name is
hierarchical, and the string is split at the dots ('.').
"a.b".toSubstring.toName is the name a.b, not Β«a.bΒ». For the latter, use
Name.mkSimple β Substring.toString.
String.getUtf8Byte (s : String) (n : Nat) (h : n < s.utf8ByteSize) : UInt8
Accesses the indicated byte in the UTF-8 encoding of a string.
At runtime, this function is implemented by efficient, constant-time code.
String.utf8ByteSize : String β Nat
The number of bytes used by the string's UTF-8 encoding.
At runtime, this function takes constant time because the byte length of strings is cached.
String.utf8EncodeChar (c : Char) : List UInt8
Returns the sequence of bytes in a character's UTF-8 encoding.
String.utf8DecodeChar? (a : ByteArray) (i : Nat) : Option Char
Decodes the UTF-8 character sequence that starts at a given index in a byte array, or none if
index i is out of bounds or is not the start of a valid UTF-8 character.
String.fromUTF8 (a : ByteArray) (h : String.validateUTF8 a = true) : String
String.fromUTF8! (a : ByteArray) : String
Decodes an array of bytes that encode a string as UTF-8 into the corresponding string, or panics if the array is not a valid UTF-8 encoding of a string.
String.validateUTF8 (a : ByteArray) : Bool
Checks whether an array of bytes is a valid UTF-8 encoding of a string.
String.crlfToLf (text : String) : String
Replaces each \r\n with \n to normalize line endings, but does not validate that there are no
isolated \r characters.
This is an optimized version of String.replace text "\r\n" "\n".
typedef struct {
lean_object m_header;
/* byte length including '\0' terminator */
size_t m_size;
size_t m_capacity;
/* UTF8 length */
size_t m_length;
char m_data[0];
} lean_string_object;
The representation of strings in C. See the description of run-time Strings for more details.
bool lean_is_string(lean_object * o)
Returns true if o is a string, or false otherwise.
lean_string_object * lean_to_string(lean_object * o)
Performs a runtime check that o is indeed a string. If o is not a string, an assertion fails.