String.append : String → String → String

Appends two strings.

The internal implementation uses dynamic arrays and will perform destructive updates if the string is not shared.

Example: "abc".append "def" = "abcdef"

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, because the compiler uses an optimized representation as dynamic arrays.

Example: "abc".toList = ['a', 'b', 'c']

String.toNat! (s : String) : Nat

Interpret the string as the decimal representation of a natural number.

Panics if the string is not a string of digits.

String.length : String → Nat

Returns the length of a string in Unicode code points.

Examples:

• "".length = 0

• "abc".length = 3

• "L∃∀N".length = 4

String.Pos : Type

A byte position in a String. Internally, Strings are UTF-8 encoded. Codepoint positions (counting the Unicode codepoints rather than bytes) are represented by plain Nats instead. Indexing a String by a byte position is constant-time, while codepoint positions need to be translated internally to byte positions in linear-time.

A byte position p is valid for a string s if 0 ≤ p ≤ s.endPos and p lies on a UTF8 byte boundary.

Constructor

String.Pos.mk (byteIdx : Nat) : String.Pos

Fields

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, meaning that p ≤ s.endPos and p lies on a UTF-8 character boundary. This has an O(1) implementation in the runtime.

String.atEnd : String → String.Pos → Bool

Returns true if a specified position is greater than or equal to the position which points to the end of a string. Otherwise, returns false.

Examples: Given def abc := "abc" and def lean := "L∃∀N",

• (0 |> abc.next |> abc.next |> abc.atEnd) = false

• (0 |> abc.next |> abc.next |> abc.next |> abc.next |> abc.atEnd) = true

• (0 |> lean.next |> lean.next |> lean.next |> lean.next |> lean.atEnd) = true

Because "L∃∀N" contains multi-byte characters, lean.next (lean.next 0) is not equal to abc.next (abc.next 0).

String.endPos (s : String) : String.Pos

A String.Pos pointing at the end of this string.

String.next (s : String) (p : String.Pos)
    : String.Pos

Returns the next position in a string after position p. If p is not a valid position or p = s.endPos, the result is unspecified.

Examples: Given def abc := "abc" and def lean := "L∃∀N",

• abc.get (0 |> abc.next) = 'b'

• lean.get (0 |> lean.next |> lean.next) = '∀'

Cases where the result is unspecified:

• "abc".next ⟨3⟩, since 3 = s.endPos

• "L∃∀N".next ⟨2⟩, since 2 points into the middle of a multi-byte UTF-8 character

String.next' (s : String) (p : String.Pos)
    (h : ¬s.atEnd p = true) : String.Pos

Returns the next position in a string after position p. If p is not a valid position, the result is unspecified.

Requires evidence, h, that p is within bounds instead of performing a runtime bounds check as in next.

Examples:

• let abc := "abc"; abc.get (abc.next' 0 (by decide)) = 'b'

A typical pattern combines next' with a dependent if-else 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)

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.

Examples: Given def abc := "abc" and def lean := "L∃∀N",

• abc.get (abc.endPos |> abc.prev) = 'c'

• lean.get (lean.endPos |> lean.prev |> lean.prev |> lean.prev) = '∃'

• "L∃∀N".prev ⟨3⟩ is unspecified, since byte 3 occurs in the middle of the multi-byte character '∃'.

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 (default : Char).

See utf8GetAux for the reference implementation.

Examples:

• "abc".get ⟨1⟩ = 'b'

• "abc".get ⟨3⟩ = (default : Char) = 'A'

Positions can also be invalid if a byte index points into the middle of a multi-byte UTF-8 character. For example,"L∃∀N".get ⟨2⟩ = (default : Char) = 'A'.

String.get? : String → String.Pos → Option Char

Returns the character at position p. If p is not a valid position, returns none.

Examples:

• "abc".get? ⟨1⟩ = some 'b'

• "abc".get? ⟨3⟩ = none

Positions can also be invalid if a byte index points into the middle of a multi-byte UTF-8 character. For example, "L∃∀N".get? ⟨2⟩ = none

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 (default : Char) and produces a panic error message.

Examples:

• "abc".get! ⟨1⟩ = 'b'

• "abc".get! ⟨3⟩ panics

Positions can also be invalid if a byte index points into the middle of a multi-byte UTF-8 character. For example, "L∃∀N".get! ⟨2⟩ panics.

String.get' (s : String) (p : String.Pos)
    (h : ¬s.atEnd p = true) : Char

Returns the character at position p of a string. If p is not a valid position, returns (default : Char).

Requires evidence, h, that p is within bounds instead of performing a runtime bounds check as in get.

Examples:

• "abc".get' 0 (by decide) = 'a'

• let lean := "L∃∀N"; lean.get' (0 |> lean.next |> lean.next) (by decide) = '∀'

A typical pattern combines get' with a dependent if-else 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).

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 ASCII characters and the string is not shared, destructive updates are used.

Examples:

• "abc".set ⟨1⟩ 'B' = "aBc"

• "abc".set ⟨3⟩ 'D' = "abc"

• "L∃∀N".set ⟨4⟩ 'X' = "L∃XN"

Because '∃' is a multi-byte character, the byte index 2 in L∃∀N is an invalid position, so "L∃∀N".set ⟨2⟩ 'X' = "L∃∀N".

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.

Examples:

• abc.modify ⟨1⟩ Char.toUpper = "aBc"

• abc.modify ⟨3⟩ Char.toUpper = "abc"

String.front (s : String) : Char

Returns the first character in s. If s = "", returns (default : Char).

Examples:

• "abc".front = 'a'

• "".front = (default : Char)

String.back (s : String) : Char

Returns the last character in s. If s = "", returns (default : Char).

Examples:

• "abc".back = 'c'

• "".back = (default : Char)

String.posOf (s : String) (c : Char)
    : String.Pos

Returns the position of the first occurrence of a character, c, in s. If s does not contain c, returns s.endPos.

Examples:

• "abba".posOf 'a' = ⟨0⟩

• "abba".posOf 'z' = ⟨4⟩

• "L∃∀N".posOf '∀' = ⟨4⟩

String.revPosOf (s : String) (c : Char)
    : Option String.Pos

Returns the position of the last occurrence of a character, c, in s. If s does not contain c, returns none.

Examples:

• "abba".posOf 'a' = some ⟨3⟩

• "abba".posOf 'z' = none

• "L∃∀N".posOf '∀' = some ⟨4⟩

String.replace (s pattern replacement : String)
    : String

Replace all occurrences of pattern in s with replacement.

String.findLineStart (s : String)
    (pos : String.Pos) : String.Pos

Return the beginning of the line that contains character pos.

String.firstDiffPos (a b : String) : String.Pos

Returns the first position where the two strings differ.

String.substrEq (s1 : String)
    (off1 : String.Pos) (s2 : String)
    (off2 : String.Pos) (sz : Nat) : Bool

Return true iff the substring of byte size sz starting at position off1 in s1 is equal to that starting at off2 in s2.. False if either substring of that byte size does not exist.

String.isPrefixOf (p s : String) : Bool

Return true iff p is a prefix of s

String.decEq (s₁ s₂ : String)
    : Decidable (s₁ = s₂)

Decides equality on String. This function is overridden with a native implementation.

String.hash (s : String) : UInt64

An opaque string hash function.

String.splitOn (s : String)
  (sep : String := " ") : List String

Splits a string s on occurrences of the separator sep. When sep is empty, it returns [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 nonoverlapping matches of sep in the string. The default separator is " ". The separators are not included in the returned substrings.

"here is some text ".splitOn = ["here", "is", "some", "text", ""]
"here is some text ".splitOn "some" = ["here is ", " text "]
"here is some text ".splitOn "" = ["here is some text "]
"ababacabac".splitOn "aba" = ["", "bac", "c"]

String.push : String → Char → String

Pushes a character onto the end of a string.

The internal implementation uses dynamic arrays and will perform destructive updates if the string is not shared.

Example: "abc".push 'd' = "abcd"

String.Iterator : Type

Iterator over the characters (Char) of a String.

Typically created by s.iter, where s is a String.

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 arbitrary values if the iterator is not valid. The functions in the String.Iterator API should 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.

Constructor

String.Iterator.mk (s : String) (i : String.Pos) : String.Iterator

Fields

i	:	String.Pos
		The current position. This position is not necessarily valid for the string, for instance if one keeps calling Iterator.next when Iterator.atEnd is true. If the position is not valid, then the current character is (default : Char), similar to String.get on an invalid position.
s	:	String
		The string the iterator is for.

String.iter (s : String) : String.Iterator

Creates an iterator at the beginning of a string.

String.mkIterator (s : String) : String.Iterator

Creates an iterator at the beginning of a string.

String.Iterator.curr : String.Iterator → Char

The character at the current position.

On an invalid position, returns (default : Char).

String.Iterator.hasNext : String.Iterator → Bool

True if the iterator is not past 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. Iterator.atEnd is false; otherwise, the resulting iterator will be invalid.

String.Iterator.forward
    : String.Iterator → Nat → String.Iterator

Moves the iterator's position several characters forward.

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 several characters forward.

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

True if the position is not zero.

String.Iterator.prev
    : String.Iterator → String.Iterator

Decreases the iterator's position.

If the position is zero, this function is the identity.

String.Iterator.prevn
    : String.Iterator → Nat → String.Iterator

Moves the iterator's position several characters back.

If asked to go back more characters than available, stops at the beginning of the string.

String.Iterator.atEnd : String.Iterator → Bool

True if the iterator is past the string's last character.

String.Iterator.toEnd
    : String.Iterator → String.Iterator

Moves the iterator's position to the end of the string.

Note that i.toEnd.atEnd is always true.

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 the iterator contains the only reference to its string, this function will mutate the string in-place instead of allocating a new one.

String.Iterator.extract
    : String.Iterator → String.Iterator → String

Extracts the substring between the positions of two iterators.

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

Number of bytes remaining in the iterator.

String.Iterator.pos (self : String.Iterator)
    : String.Pos

The current position.

This position is not necessarily valid for the string, for instance if one keeps calling Iterator.next when Iterator.atEnd is true. 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

Convert a String into a Substring denoting the entire string.

String.toSubstring' (s : String) : Substring

String.toSubstring without [inline] annotation.

String.toName (s : String) : Lean.Name

Converts a String to a hierarchical Name after splitting it at the dots.

"a.b".toName is the name a.b, not «a.b». For the latter, use Name.mkSimple.

String.utf16PosToCodepointPosFrom (s : String)
    (utf16pos : Nat) (off : String.Pos) : Nat

Computes the position of the Unicode codepoint at UTF-16 offset utf16pos in the substring of s starting at UTF-8 offset off.

String.codepointPosToUtf16PosFrom (s : String)
    (n : Nat) (off : String.Pos) : Nat

Computes the UTF-16 offset of the n-th Unicode codepoint in the substring of s starting at UTF-8 offset off. Yes, this is actually useful.

String.getUtf8Byte (s : String) (n : Nat)
    (h : n < s.utf8ByteSize) : UInt8

Accesses a byte in the UTF-8 encoding of the String. O(1)

String.utf8ByteSize : String → Nat

The UTF-8 byte length of this string. This is overridden by the compiler to be cached and O(1).

String.fromUTF8 (a : ByteArray)
    (h : String.validateUTF8 a = true) : String

Converts a UTF-8 encoded ByteArray string to String.

String.fromUTF8? (a : ByteArray) : Option String

Converts a UTF-8 encoded ByteArray string to String, or returns none if a is not properly UTF-8 encoded.

String.fromUTF8! (a : ByteArray) : String

Converts a UTF-8 encoded ByteArray string to String, or panics if a is not properly UTF-8 encoded.

String.toUTF8 (a : String) : ByteArray

Converts the given String to a UTF-8 encoded byte array.

String.validateUTF8 (a : ByteArray) : Bool

Returns true if the given byte array consists of valid UTF-8.

String.codepointPosToUtf8PosFrom (s : String)
    : String.Pos → Nat → String.Pos

Starting at utf8pos, finds the UTF-8 offset of the p-th codepoint.

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. It is an optimized version of String.replace text "\r\n" "\n".