def List.asString (s : List Char) : String

Equations

• s.asString = { data := s }

instance String.instOfNatPos : OfNat String.Pos 0

Equations

• String.instOfNatPos = { ofNat := { byteIdx := 0 } }

instance String.instLT : LT String

Equations

• String.instLT = { lt := fun (s₁ s₂ : String) => s₁.data < s₂.data }

@[extern lean_string_dec_lt]

instance String.decLt (s₁ : String) (s₂ : String) : Decidable (s₁ < s₂)

Equations

• s₁.decLt s₂ = s₁.data.hasDecidableLt s₂.data

@[reducible]

def String.le (a : String) (b : String) : Prop

Equations

• a.le b = ¬b < a

instance String.instLE : LE String

Equations

• String.instLE = { le := String.le }

instance String.decLE (s₁ : String) (s₂ : String) : Decidable (s₁ ≤ s₂)

Equations

• s₁.decLE s₂ = inferInstanceAs (Decidable ¬s₂ < s₁)

@[extern lean_string_length]

def String.length : String → Nat

Returns the length of a string in Unicode code points.

Examples:

• "".length = 0
• "abc".length = 3
• "L∃∀N".length = 4

Equations

• x.length = match x with | { data := s } => s.length

@[extern lean_string_push]

def 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"

Equations

• x✝.push x = match x✝, x with | { data := s }, c => { data := s ++ [c] }

@[extern lean_string_append]

def 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"

Equations

• x✝.append x = match x✝, x with | { data := a }, { data := b } => { data := a ++ b }

def 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']

Equations

• s.toList = s.data

@[extern lean_string_is_valid_pos]

def 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.

Equations

• String.Pos.isValid s p = String.Pos.isValid.go p s.data 0

def String.Pos.isValid.go (p : String.Pos) : List Char → String.Pos → Bool

Equations

• String.Pos.isValid.go p [] x = decide (x = p)
• String.Pos.isValid.go p (c :: cs) x = if x = p then true else String.Pos.isValid.go p cs (x + c)

def String.utf8GetAux : List Char → String.Pos → String.Pos → Char

Equations

• String.utf8GetAux [] x✝ x = default
• String.utf8GetAux (c :: cs) x✝ x = if x✝ = x then c else String.utf8GetAux cs (x✝ + c) x

@[extern lean_string_utf8_get]

def 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'.

Equations

• s.get p = match s with | { data := s } => String.utf8GetAux s 0 p

def String.utf8GetAux? : List Char → String.Pos → String.Pos → Option Char

Equations

• String.utf8GetAux? [] x✝ x = none
• String.utf8GetAux? (c :: cs) x✝ x = if x✝ = x then some c else String.utf8GetAux? cs (x✝ + c) x

@[extern lean_string_utf8_get_opt]

def 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

Equations

• x✝.get? x = match x✝, x with | { data := s }, p => String.utf8GetAux? s 0 p

@[extern lean_string_utf8_get_bang]

def 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.

Equations

• s.get! p = match s with | { data := s } => String.utf8GetAux s 0 p

def String.utf8SetAux (c' : Char) : List Char → String.Pos → String.Pos → List Char

Equations

• String.utf8SetAux c' [] x✝ x = []
• String.utf8SetAux c' (c :: cs) x✝ x = if x✝ = x then c' :: cs else c :: String.utf8SetAux c' cs (x✝ + c) x

@[extern lean_string_utf8_set]

def 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".

Equations

• x✝¹.set x✝ x = match x✝¹, x✝, x with | { data := s }, i, c => { data := String.utf8SetAux c s 0 i }

def 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"

Equations

• s.modify i f = s.set i (f (s.get i))

@[extern lean_string_utf8_next]

def 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

Equations

• s.next p = let c := s.get p; p + c

def String.utf8PrevAux : List Char → String.Pos → String.Pos → String.Pos

Equations

• String.utf8PrevAux [] x✝ x = 0
• String.utf8PrevAux (c :: cs) x✝ x = let i' := x✝ + c; if i' = x then x✝ else String.utf8PrevAux cs i' x

@[extern lean_string_utf8_prev]

def 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 '∃'.

Equations

• x✝.prev x = match x✝, x with | { data := s }, p => if p = 0 then 0 else String.utf8PrevAux s 0 p

def String.front (s : String) : Char

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

Examples:

• "abc".front = 'a'
• "".front = (default : Char)

Equations

• s.front = s.get 0

def String.back (s : String) : Char

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

Examples:

• "abc".back = 'c'
• "".back = (default : Char)

Equations

• s.back = s.get (s.prev s.endPos)

@[extern lean_string_utf8_at_end]

def 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).

Equations

• x✝.atEnd x = match x✝, x with | s, p => decide (p.byteIdx ≥ s.utf8ByteSize)

@[extern lean_string_utf8_get_fast]

def 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).

Equations

• s.get' p h = match s, h with | { data := s }, h => String.utf8GetAux s 0 p

@[extern lean_string_utf8_next_fast]

def 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)

Equations

• s.next' p h = let c := s.get p; p + c

theorem Char.utf8Size_pos (c : Char) : 0 < c.utf8Size

theorem Char.utf8Size_le_four (c : Char) : c.utf8Size ≤ 4

@[reducible, inline, deprecated Char.utf8Size_pos]

abbrev String.one_le_csize (c : Char) : 0 < c.utf8Size

Equations

• String.one_le_csize = Char.utf8Size_pos

@[simp]

theorem String.pos_lt_eq (p₁ : String.Pos) (p₂ : String.Pos) : (p₁ < p₂) = (p₁.byteIdx < p₂.byteIdx)

@[simp]

theorem String.pos_add_char (p : String.Pos) (c : Char) : (p + c).byteIdx = p.byteIdx + c.utf8Size

theorem String.lt_next (s : String) (i : String.Pos) : i.byteIdx < (s.next i).byteIdx

theorem String.utf8PrevAux_lt_of_pos (cs : List Char) (i : String.Pos) (p : String.Pos) : p ≠ 0 → (String.utf8PrevAux cs i p).byteIdx < p.byteIdx

theorem String.prev_lt_of_pos (s : String) (i : String.Pos) (h : i ≠ 0) : (s.prev i).byteIdx < i.byteIdx

@[irreducible]

def String.posOfAux (s : String) (c : Char) (stopPos : String.Pos) (pos : String.Pos) : String.Pos

Equations

• s.posOfAux c stopPos pos = if h : pos < stopPos then if (s.get pos == c) = true then pos else let_fun this := ⋯; s.posOfAux c stopPos (s.next pos) else pos

@[inline]

def 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⟩

Equations

• s.posOf c = s.posOfAux c s.endPos 0

@[irreducible]

def String.revPosOfAux (s : String) (c : Char) (pos : String.Pos) : Option String.Pos

Equations

• s.revPosOfAux c pos = if h : pos = 0 then none else let_fun this := ⋯; let pos := s.prev pos; if (s.get pos == c) = true then some pos else s.revPosOfAux c pos

def 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⟩

Equations

• s.revPosOf c = s.revPosOfAux c s.endPos

@[irreducible]

def String.findAux (s : String) (p : Char → Bool) (stopPos : String.Pos) (pos : String.Pos) : String.Pos

Equations

• s.findAux p stopPos pos = if h : pos < stopPos then if p (s.get pos) = true then pos else let_fun this := ⋯; s.findAux p stopPos (s.next pos) else pos

@[inline]

def String.find (s : String) (p : Char → Bool) : String.Pos

Equations

• s.find p = s.findAux p s.endPos 0

@[irreducible]

def String.revFindAux (s : String) (p : Char → Bool) (pos : String.Pos) : Option String.Pos

Equations

• s.revFindAux p pos = if h : pos = 0 then none else let_fun this := ⋯; let pos := s.prev pos; if p (s.get pos) = true then some pos else s.revFindAux p pos

def String.revFind (s : String) (p : Char → Bool) : Option String.Pos

Equations

• s.revFind p = s.revFindAux p s.endPos

@[reducible, inline]

abbrev String.Pos.min (p₁ : String.Pos) (p₂ : String.Pos) : String.Pos

Equations

• p₁.min p₂ = { byteIdx := p₁.byteIdx.min p₂.byteIdx }

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

Returns the first position where the two strings differ.

Equations

• a.firstDiffPos b = let stopPos := a.endPos.min b.endPos; String.firstDiffPos.loop a b stopPos 0

@[irreducible]

def String.firstDiffPos.loop (a : String) (b : String) (stopPos : String.Pos) (i : String.Pos) : String.Pos

Equations

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

@[extern lean_string_utf8_extract]

def String.extract : String → String.Pos → String.Pos → String

Equations

• x✝¹.extract x✝ x = match x✝¹, x✝, x with | { data := s }, b, e => if b.byteIdx ≥ e.byteIdx then "" else { data := String.extract.go₁ s 0 b e }

def String.extract.go₁ : List Char → String.Pos → String.Pos → String.Pos → List Char

Equations

• String.extract.go₁ [] x✝¹ x✝ x = []
• String.extract.go₁ (c :: cs) x✝¹ x✝ x = if x✝¹ = x✝ then String.extract.go₂ (c :: cs) x✝¹ x else String.extract.go₁ cs (x✝¹ + c) x✝ x

def String.extract.go₂ : List Char → String.Pos → String.Pos → List Char

Equations

• String.extract.go₂ [] x✝ x = []
• String.extract.go₂ (c :: cs) x✝ x = if x✝ = x then [] else c :: String.extract.go₂ cs (x✝ + c) x

@[irreducible, specialize #[]]

def String.splitAux (s : String) (p : Char → Bool) (b : String.Pos) (i : String.Pos) (r : List String) : List String

Equations

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

@[specialize #[]]

def String.split (s : String) (p : Char → Bool) : List String

Equations

• s.split p = s.splitAux p 0 0 []

@[irreducible]

def String.splitOnAux (s : String) (sep : String) (b : String.Pos) (i : String.Pos) (j : String.Pos) (r : List String) : List String

Auxiliary for splitOn. Preconditions:

• sep is not empty
• b <= i are indexes into s
• j is an index into sep, and not at the end

It represents the state where we have currently parsed some split parts into r (in reverse order), b is the beginning of the string / the end of the previous match of sep, and the first j bytes of sep match the bytes i-j .. i of s.

Equations

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

def String.splitOn (s : String) (sep : optParam 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"]

Equations

• s.splitOn sep = if (sep == "") = true then [s] else s.splitOnAux sep 0 0 0 []

instance String.instInhabited : Inhabited String

Equations

• String.instInhabited = { default := "" }

instance String.instAppend : Append String

Equations

• String.instAppend = { append := String.append }

@[deprecated String.push]

def String.str : String → Char → String

Equations

• String.str = String.push

def String.pushn (s : String) (c : Char) (n : Nat) : String

Equations

• s.pushn c n = Nat.repeat (fun (s : String) => s.push c) n s

def String.isEmpty (s : String) : Bool

Equations

• s.isEmpty = (s.endPos == 0)

def String.join (l : List String) : String

Equations

• String.join l = List.foldl (fun (r s : String) => r ++ s) "" l

def String.singleton (c : Char) : String

Equations

• String.singleton c = "".push c

def String.intercalate (s : String) : List String → String

Equations

• s.intercalate x = match x with | [] => "" | a :: as => String.intercalate.go a s as

def String.intercalate.go (acc : String) (s : String) : List String → String

Equations

• String.intercalate.go acc s (a :: as) = String.intercalate.go (acc ++ s ++ a) s as
• String.intercalate.go acc s [] = acc

structure 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.

• s : String

  The string the iterator is for.

• 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.

instance String.instDecidableEqIterator : DecidableEq String.Iterator

Equations

• String.instDecidableEqIterator = String.decEqIterator✝

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

Creates an iterator at the beginning of a string.

Equations

• s.mkIterator = { s := s, i := 0 }

@[reducible, inline]

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

Creates an iterator at the beginning of a string.

Equations

• String.iter = String.mkIterator

instance String.instSizeOfIterator : SizeOf String.Iterator

The size of a string iterator is the number of bytes remaining.

Equations

• String.instSizeOfIterator = { sizeOf := fun (i : String.Iterator) => i.s.utf8ByteSize - i.i.byteIdx }

theorem String.Iterator.sizeOf_eq (i : String.Iterator) : sizeOf i = i.s.utf8ByteSize - i.i.byteIdx

def String.Iterator.toString (self : String.Iterator) : String

The string the iterator is for.

Equations

• String.Iterator.toString = String.Iterator.s

def String.Iterator.remainingBytes : String.Iterator → Nat

Number of bytes remaining in the iterator.

Equations

• x.remainingBytes = match x with | { s := s, i := i } => s.endPos.byteIdx - i.byteIdx

def 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.

Equations

• String.Iterator.pos = String.Iterator.i

def String.Iterator.curr : String.Iterator → Char

The character at the current position.

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

Equations

• x.curr = match x with | { s := s, i := i } => s.get i

def 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.

Equations

• x.next = match x with | { s := s, i := i } => { s := s, i := s.next i }

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

Decreases the iterator's position.

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

Equations

• x.prev = match x with | { s := s, i := i } => { s := s, i := s.prev i }

def String.Iterator.atEnd : String.Iterator → Bool

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

Equations

• x.atEnd = match x with | { s := s, i := i } => decide (i.byteIdx ≥ s.endPos.byteIdx)

def String.Iterator.hasNext : String.Iterator → Bool

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

Equations

• x.hasNext = match x with | { s := s, i := i } => decide (i.byteIdx < s.endPos.byteIdx)

def String.Iterator.hasPrev : String.Iterator → Bool

True if the position is not zero.

Equations

• x.hasPrev = match x with | { s := s, i := i } => decide (i.byteIdx > 0)

def 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.

Equations

• x✝.setCurr x = match x✝, x with | { s := s, i := i }, c => { s := s.set i c, i := i }

def 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.

Equations

• x.toEnd = match x with | { s := s, i := i } => { s := s, i := s.endPos }

def 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.

Equations

• x✝.extract x = match x✝, x with | { s := s₁, i := b }, { s := s₂, i := e } => if (decide (s₁ ≠ s₂) || decide (b > e)) = true then "" else s₁.extract b e

def 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.

Equations

• x.forward 0 = x
• x.forward n.succ = x.next.forward n

def String.Iterator.remainingToString : String.Iterator → String

The remaining characters in an iterator, as a string.

Equations

• x.remainingToString = match x with | { s := s, i := i } => s.extract i s.endPos

def 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.

Equations

• x.nextn 0 = x
• x.nextn n.succ = x.next.nextn n

def 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.

Equations

• x.prevn 0 = x
• x.prevn n.succ = x.prev.prevn n

@[irreducible]

def String.offsetOfPosAux (s : String) (pos : String.Pos) (i : String.Pos) (offset : Nat) : Nat

Equations

• s.offsetOfPosAux pos i offset = if i ≥ pos then offset else if h : s.atEnd i = true then offset else let_fun this := ⋯; s.offsetOfPosAux pos (s.next i) (offset + 1)

def String.offsetOfPos (s : String) (pos : String.Pos) : Nat

Equations

• s.offsetOfPos pos = s.offsetOfPosAux pos 0 0

@[irreducible, specialize #[]]

def String.foldlAux {α : Type u} (f : α → Char → α) (s : String) (stopPos : String.Pos) (i : String.Pos) (a : α) : α

Equations

• String.foldlAux f s stopPos i a = if h : i < stopPos then let_fun this := ⋯; String.foldlAux f s stopPos (s.next i) (f a (s.get i)) else a

@[inline]

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

Equations

• String.foldl f init s = String.foldlAux f s s.endPos 0 init

@[irreducible, specialize #[]]

def String.foldrAux {α : Type u} (f : Char → α → α) (a : α) (s : String) (i : String.Pos) (begPos : String.Pos) : α

Equations

• String.foldrAux f a s i begPos = if h : begPos < i then let_fun this := ⋯; let i := s.prev i; let a := f (s.get i) a; String.foldrAux f a s i begPos else a

@[inline]

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

Equations

• String.foldr f init s = String.foldrAux f init s s.endPos 0

@[irreducible, specialize #[]]

def String.anyAux (s : String) (stopPos : String.Pos) (p : Char → Bool) (i : String.Pos) : Bool

Equations

• s.anyAux stopPos p i = if h : i < stopPos then if p (s.get i) = true then true else let_fun this := ⋯; s.anyAux stopPos p (s.next i) else false

@[inline]

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

Equations

• s.any p = s.anyAux s.endPos p 0

@[inline]

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

Equations

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

def String.contains (s : String) (c : Char) : Bool

Equations

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

theorem String.utf8SetAux_of_gt (c' : Char) (cs : List Char) {i : String.Pos} {p : String.Pos} : i > p → String.utf8SetAux c' cs i p = cs

theorem String.set_next_add (s : String) (i : String.Pos) (c : Char) (b₁ : Nat) (b₂ : Nat) (h : (s.next i).byteIdx + b₁ = s.endPos.byteIdx + b₂) : ((s.set i c).next i).byteIdx + b₁ = (s.set i c).endPos.byteIdx + b₂

theorem String.set_next_add.foo (i : String.Pos) (c : Char) (cs : List Char) (a : String.Pos) (b₁ : Nat) (b₂ : Nat) : (String.utf8GetAux cs a i).utf8Size + b₁ = String.utf8ByteSize.go cs + b₂ → (String.utf8GetAux (String.utf8SetAux c cs a i) a i).utf8Size + b₁ = String.utf8ByteSize.go (String.utf8SetAux c cs a i) + b₂

theorem String.mapAux_lemma (s : String) (i : String.Pos) (c : Char) (h : ¬s.atEnd i = true) : (s.set i c).endPos.byteIdx - ((s.set i c).next i).byteIdx < s.endPos.byteIdx - i.byteIdx

@[irreducible, specialize #[]]

def String.mapAux (f : Char → Char) (i : String.Pos) (s : String) : String

Equations

• String.mapAux f i s = if h : s.atEnd i = true then s else let c := f (s.get i); let_fun this := ⋯; let s := s.set i c; String.mapAux f (s.next i) s

@[inline]

def String.map (f : Char → Char) (s : String) : String

Equations

• String.map f s = String.mapAux f 0 s

def String.isNat (s : String) : Bool

Equations

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

def String.toNat? (s : String) : Option Nat

Equations

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

def 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.

Equations

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

@[irreducible]

def String.substrEq.loop (s1 : String) (s2 : String) (off1 : String.Pos) (off2 : String.Pos) (stop1 : String.Pos) : Bool

Equations

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

def String.isPrefixOf (p : String) (s : String) : Bool

Return true iff p is a prefix of s

Equations

• p.isPrefixOf s = p.substrEq 0 s 0 p.endPos.byteIdx

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

Replace all occurrences of pattern in s with replacement.

Equations

• s.replace pattern replacement = if h : pattern.endPos.byteIdx = 0 then s else let_fun hPatt := ⋯; String.replace.loop s pattern replacement hPatt "" 0 0

@[irreducible]

def String.replace.loop (s : String) (pattern : String) (replacement : String) (hPatt : 0 < pattern.endPos.byteIdx) (acc : String) (accStop : String.Pos) (pos : String.Pos) : String

Equations

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

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

Return the beginning of the line that contains character pos.

Equations

• s.findLineStart pos = match s.revFindAux (fun (x : Char) => decide (x = '\n')) pos with | none => 0 | some n => { byteIdx := n.byteIdx + 1 }

@[inline]

def Substring.isEmpty (ss : Substring) : Bool

Equations

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

@[inline]

def Substring.toString : Substring → String

Equations

• x.toString = match x with | { str := s, startPos := b, stopPos := e } => s.extract b e

@[inline]

def Substring.toIterator : Substring → String.Iterator

Equations

• x.toIterator = match x with | { str := s, startPos := b, stopPos := stopPos } => { s := s, i := b }

@[inline]

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

Return the codepoint at the given offset into the substring.

Equations

• x✝.get x = match x✝, x with | { str := s, startPos := b, stopPos := stopPos }, p => s.get (b + p)

@[inline]

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

Given an offset of a codepoint into the substring, return the offset there of the next codepoint.

Equations

• x✝.next x = match x✝, x with | { str := s, startPos := b, stopPos := e }, p => let absP := b + p; if absP = e then p else { byteIdx := (s.next absP).byteIdx - b.byteIdx }

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

@[inline]

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

Given an offset of a codepoint into the substring, return the offset there of the previous codepoint.

Equations

• x✝.prev x = match x✝, x with | { str := s, startPos := b, stopPos := stopPos }, p => let absP := b + p; if absP = b then p else { byteIdx := (s.prev absP).byteIdx - b.byteIdx }

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

Equations

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

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

Equations

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

@[inline]

def Substring.front (s : Substring) : Char

Equations

• s.front = s.get 0

@[inline]

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

Return the offset into s of the first occurrence of c in s, or s.bsize if c doesn't occur.

Equations

• s.posOf c = match s with | { str := s, startPos := b, stopPos := e } => { byteIdx := (s.posOfAux c e b).byteIdx - b.byteIdx }

@[inline]

def Substring.drop : Substring → Nat → Substring

Equations

• x✝.drop x = match x✝, x with | ss@h:{ str := s, startPos := b, stopPos := e }, n => { str := s, startPos := b + ss.nextn n 0, stopPos := e }

@[inline]

def Substring.dropRight : Substring → Nat → Substring

Equations

• x✝.dropRight x = match x✝, x with | ss@h:{ str := s, startPos := b, stopPos := stopPos }, n => { str := s, startPos := b, stopPos := b + ss.prevn n { byteIdx := ss.bsize } }

@[inline]

def Substring.take : Substring → Nat → Substring

Equations

• x✝.take x = match x✝, x with | ss@h:{ str := s, startPos := b, stopPos := stopPos }, n => { str := s, startPos := b, stopPos := b + ss.nextn n 0 }

@[inline]

def Substring.takeRight : Substring → Nat → Substring

Equations

• x✝.takeRight x = match x✝, x with | ss@h:{ str := s, startPos := b, stopPos := e }, n => { str := s, startPos := b + ss.prevn n { byteIdx := ss.bsize }, stopPos := e }

@[inline]

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

Equations

• x✝.atEnd x = match x✝, x with | { str := str, startPos := b, stopPos := e }, p => b + p == e

@[inline]

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

Equations

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

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

Equations

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

@[irreducible]

def Substring.splitOn.loop (s : Substring) (sep : optParam String " ") (b : String.Pos) (i : String.Pos) (j : String.Pos) (r : List Substring) : List Substring

Equations

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

@[inline]

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

Equations

• Substring.foldl f init s = match s with | { str := s, startPos := b, stopPos := e } => String.foldlAux f s e b init

@[inline]

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

Equations

• Substring.foldr f init s = match s with | { str := s, startPos := b, stopPos := e } => String.foldrAux f init s e b

@[inline]

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

Equations

• s.any p = match s with | { str := s, startPos := b, stopPos := e } => s.anyAux e p b

@[inline]

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

Equations

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

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

Equations

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

@[irreducible, specialize #[]]

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

Equations

• Substring.takeWhileAux s stopPos p i = if h : i < stopPos then if p (s.get i) = true then let_fun this := ⋯; Substring.takeWhileAux s stopPos p (s.next i) else i else i

@[inline]

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

Equations

• x✝.takeWhile x = match x✝, x with | { str := s, startPos := b, stopPos := e }, p => let e := Substring.takeWhileAux s e p b; { str := s, startPos := b, stopPos := e }

@[inline]

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

Equations

• x✝.dropWhile x = match x✝, x with | { str := s, startPos := b, stopPos := e }, p => let b := Substring.takeWhileAux s e p b; { str := s, startPos := b, stopPos := e }

@[irreducible, specialize #[]]

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

Equations

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

@[inline]

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

Equations

• x✝.takeRightWhile x = match x✝, x with | { str := s, startPos := b, stopPos := e }, p => let b := Substring.takeRightWhileAux s b p e; { str := s, startPos := b, stopPos := e }

@[inline]

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

Equations

• x✝.dropRightWhile x = match x✝, x with | { str := s, startPos := b, stopPos := e }, p => let e := Substring.takeRightWhileAux s b p e; { str := s, startPos := b, stopPos := e }

@[inline]

def Substring.trimLeft (s : Substring) : Substring

Equations

• s.trimLeft = s.dropWhile Char.isWhitespace

@[inline]

def Substring.trimRight (s : Substring) : Substring

Equations

• s.trimRight = s.dropRightWhile Char.isWhitespace

@[inline]

def Substring.trim : Substring → Substring

Equations

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

def Substring.isNat (s : Substring) : Bool

Equations

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

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

Equations

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

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

Equations

• ss1.beq ss2 = (ss1.bsize == ss2.bsize && ss1.str.substrEq ss1.startPos ss2.str ss2.startPos ss1.bsize)

instance Substring.hasBeq : BEq Substring

Equations

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

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

Checks whether two substrings have the same position and content.

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def String.trimRight (s : String) : String

Equations

• s.trimRight = s.toSubstring.trimRight.toString

def String.trimLeft (s : String) : String

Equations

• s.trimLeft = s.toSubstring.trimLeft.toString

def String.trim (s : String) : String

Equations

• s.trim = s.toSubstring.trim.toString

@[inline]

def String.nextWhile (s : String) (p : Char → Bool) (i : String.Pos) : String.Pos

Equations

• s.nextWhile p i = Substring.takeWhileAux s s.endPos p i

@[inline]

def String.nextUntil (s : String) (p : Char → Bool) (i : String.Pos) : String.Pos

Equations

• s.nextUntil p i = s.nextWhile (fun (c : Char) => !p c) i

def String.toUpper (s : String) : String

Equations

• s.toUpper = String.map Char.toUpper s

def String.toLower (s : String) : String

Equations

• s.toLower = String.map Char.toLower s

def String.capitalize (s : String) : String

Equations

• s.capitalize = s.set 0 (s.get 0).toUpper

def String.decapitalize (s : String) : String

Equations

• s.decapitalize = s.set 0 (s.get 0).toLower

def Char.toString (c : Char) : String

Equations

• c.toString = String.singleton c

@[simp]

theorem Char.length_toString (c : Char) : c.toString.length = 1

theorem String.ext {s₁ : String} {s₂ : String} (h : s₁.data = s₂.data) : s₁ = s₂

theorem String.ext_iff {s₁ : String} {s₂ : String} : s₁ = s₂ ↔ s₁.data = s₂.data

@[simp]

theorem String.default_eq : default = ""

@[simp]

theorem String.length_mk (s : List Char) : { data := s }.length = s.length

@[simp]

theorem String.length_empty : "".length = 0

@[simp]

theorem String.length_singleton (c : Char) : (String.singleton c).length = 1

@[simp]

theorem String.length_push {s : String} (c : Char) : (s.push c).length = s.length + 1

@[simp]

theorem String.length_pushn {s : String} (c : Char) (n : Nat) : (s.pushn c n).length = s.length + n

@[simp]

theorem String.length_append (s : String) (t : String) : (s ++ t).length = s.length + t.length

@[simp]

theorem String.data_push (s : String) (c : Char) : (s.push c).data = s.data ++ [c]

@[simp]

theorem String.data_append (s : String) (t : String) : (s ++ t).data = s.data ++ t.data

theorem String.lt_iff (s : String) (t : String) : s < t ↔ s.data < t.data

@[simp]

theorem String.Pos.byteIdx_zero : String.Pos.byteIdx 0 = 0

theorem String.Pos.byteIdx_mk (n : Nat) : { byteIdx := n }.byteIdx = n

@[simp]

theorem String.Pos.mk_zero : { byteIdx := 0 } = 0

@[simp]

theorem String.Pos.mk_byteIdx (p : String.Pos) : { byteIdx := p.byteIdx } = p

theorem String.Pos.ext {i₁ : String.Pos} {i₂ : String.Pos} (h : i₁.byteIdx = i₂.byteIdx) : i₁ = i₂

theorem String.Pos.ext_iff {i₁ : String.Pos} {i₂ : String.Pos} : i₁ = i₂ ↔ i₁.byteIdx = i₂.byteIdx

@[simp]

theorem String.Pos.add_byteIdx (p₁ : String.Pos) (p₂ : String.Pos) : (p₁ + p₂).byteIdx = p₁.byteIdx + p₂.byteIdx

theorem String.Pos.add_eq (p₁ : String.Pos) (p₂ : String.Pos) : p₁ + p₂ = { byteIdx := p₁.byteIdx + p₂.byteIdx }

@[simp]

theorem String.Pos.sub_byteIdx (p₁ : String.Pos) (p₂ : String.Pos) : (p₁ - p₂).byteIdx = p₁.byteIdx - p₂.byteIdx

theorem String.Pos.sub_eq (p₁ : String.Pos) (p₂ : String.Pos) : p₁ - p₂ = { byteIdx := p₁.byteIdx - p₂.byteIdx }

@[simp]

theorem String.Pos.addChar_byteIdx (p : String.Pos) (c : Char) : (p + c).byteIdx = p.byteIdx + c.utf8Size

theorem String.Pos.addChar_eq (p : String.Pos) (c : Char) : p + c = { byteIdx := p.byteIdx + c.utf8Size }

theorem String.Pos.zero_addChar_byteIdx (c : Char) : (0 + c).byteIdx = c.utf8Size

theorem String.Pos.zero_addChar_eq (c : Char) : 0 + c = { byteIdx := c.utf8Size }

theorem String.Pos.addChar_right_comm (p : String.Pos) (c₁ : Char) (c₂ : Char) : p + c₁ + c₂ = p + c₂ + c₁

theorem String.Pos.ne_of_lt {i₁ : String.Pos} {i₂ : String.Pos} (h : i₁ < i₂) : i₁ ≠ i₂

theorem String.Pos.ne_of_gt {i₁ : String.Pos} {i₂ : String.Pos} (h : i₁ < i₂) : i₂ ≠ i₁

@[simp]

theorem String.Pos.addString_byteIdx (p : String.Pos) (s : String) : (p + s).byteIdx = p.byteIdx + s.utf8ByteSize

theorem String.Pos.addString_eq (p : String.Pos) (s : String) : p + s = { byteIdx := p.byteIdx + s.utf8ByteSize }

theorem String.Pos.zero_addString_byteIdx (s : String) : (0 + s).byteIdx = s.utf8ByteSize

theorem String.Pos.zero_addString_eq (s : String) : 0 + s = { byteIdx := s.utf8ByteSize }

theorem String.Pos.le_iff {i₁ : String.Pos} {i₂ : String.Pos} : i₁ ≤ i₂ ↔ i₁.byteIdx ≤ i₂.byteIdx

@[simp]

theorem String.Pos.mk_le_mk {i₁ : Nat} {i₂ : Nat} : { byteIdx := i₁ } ≤ { byteIdx := i₂ } ↔ i₁ ≤ i₂

theorem String.Pos.lt_iff {i₁ : String.Pos} {i₂ : String.Pos} : i₁ < i₂ ↔ i₁.byteIdx < i₂.byteIdx

@[simp]

theorem String.Pos.mk_lt_mk {i₁ : Nat} {i₂ : Nat} : { byteIdx := i₁ } < { byteIdx := i₂ } ↔ i₁ < i₂

@[simp]

theorem String.get!_eq_get (s : String) (p : String.Pos) : s.get! p = s.get p

theorem String.lt_next' (s : String) (p : String.Pos) : p < s.next p

@[simp]

theorem String.prev_zero (s : String) : s.prev 0 = 0

@[simp]

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

@[simp]

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

theorem String.singleton_eq (c : Char) : String.singleton c = { data := [c] }

@[simp]

theorem String.data_singleton (c : Char) : (String.singleton c).data = [c]

@[simp]

theorem String.append_empty (s : String) : s ++ "" = s

@[simp]

theorem String.empty_append (s : String) : "" ++ s = s

theorem String.append_assoc (s₁ : String) (s₂ : String) (s₃ : String) : s₁ ++ s₂ ++ s₃ = s₁ ++ (s₂ ++ s₃)

@[simp]

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

@[simp]

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