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

instance String.instOfNatPos : OfNat String.Pos 0

instance String.instLTString : LT String

@[extern lean_string_dec_lt]

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

@[extern lean_string_length]

def String.length : String → Nat

@[extern lean_string_push]

def String.push : String → Char → String

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

@[extern lean_string_append]

def String.append : String → String → String

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

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

O(n) in the runtime, where n is the length of the String

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

Return character at position p. If p is not a valid position returns (default : Char). See utf8GetAux for the reference implementation.

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

@[extern lean_string_utf8_get_bang]

def String.get! (s : String) (p : String.Pos) : Char

Similar to get, but produces a panic error message if p is not a valid String.Pos.

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

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

@[extern lean_string_utf8_next]

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

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

def String.front (s : String) : Char

def String.back (s : String) : Char

@[extern lean_string_utf8_at_end]

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

@[extern lean_string_utf8_get_fast]

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

Similar to get but runtime does not perform bounds check.

@[extern lean_string_utf8_next_fast]

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

Similar to next but runtime does not perform bounds check.

theorem String.one_le_csize (c : Char) : 1 ≤ String.csize c

@[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 + String.csize c

theorem String.lt_next (s : String) (i : String.Pos) : i.byteIdx < (String.next s 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) : (String.prev s i).byteIdx < i.byteIdx

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

Equations

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

@[inline]

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

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

Equations

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

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

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

Equations

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

@[inline]

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

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

Equations

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

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

@[inline, reducible]

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

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

Returns the first position where the two strings differ.

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

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

@[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

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

Equations

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

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

instance String.instInhabitedString : Inhabited String

instance String.instAppendString : Append String

def String.str : String → Char → String

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

def String.isEmpty (s : String) : Bool

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

def String.singleton (c : Char) : String

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

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

• s : String
• i : String.Pos

Iterator for String. That is, a String and a position in that string.

instance String.instDecidableEqIterator : DecidableEq String.Iterator

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

@[inline, reducible]

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

instance String.instSizeOfIterator : SizeOf String.Iterator

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

def String.Iterator.toString : String.Iterator → String

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

def String.Iterator.pos : String.Iterator → String.Pos

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

def String.Iterator.next : String.Iterator → String.Iterator

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

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

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

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

def String.Iterator.setCurr : String.Iterator → Char → String.Iterator

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

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

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

Equations

• String.Iterator.forward x 0 = x
• String.Iterator.forward x (Nat.succ n) = String.Iterator.forward (String.Iterator.next x) n

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

def String.Iterator.nextn : String.Iterator → Nat → String.Iterator

Equations

• String.Iterator.nextn x 0 = x
• String.Iterator.nextn x (Nat.succ n) = String.Iterator.nextn (String.Iterator.next x) n

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

Equations

• String.Iterator.prevn x 0 = x
• String.Iterator.prevn x (Nat.succ n) = String.Iterator.prevn (String.Iterator.prev x) n

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

Equations

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

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

@[specialize #[]]

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

Equations

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

@[inline]

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

@[specialize #[]]

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

Equations

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

@[inline]

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

@[specialize #[]]

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

Equations

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

@[inline]

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

@[inline]

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

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

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 : (String.next s i).byteIdx + b₁ = (String.endPos s).byteIdx + b₂) : (String.next (String.set s i c) i).byteIdx + b₁ = (String.endPos (String.set s i c)).byteIdx + b₂

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

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

@[specialize #[]]

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

Equations

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

@[inline]

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

def String.isNat (s : String) : Bool

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

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.

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

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

Replace all occurrences of pattern in s with replacement.

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

Equations

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

@[inline]

def Substring.isEmpty (ss : Substring) : Bool

@[inline]

def Substring.toString : Substring → String

@[inline]

def Substring.toIterator : Substring → String.Iterator

@[inline]

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

Return the codepoint at the given offset into the substring.

@[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.

theorem Substring.lt_next (s : Substring) (i : String.Pos) (h : i.byteIdx < Substring.bsize s) : i.byteIdx < (Substring.next s 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.

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

Equations

• Substring.nextn x 0 x = x
• Substring.nextn x (Nat.succ i) x = Substring.nextn x i (Substring.next x x)

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

Equations

• Substring.prevn x 0 x = x
• Substring.prevn x (Nat.succ i) x = Substring.prevn x i (Substring.prev x x)

@[inline]

def Substring.front (s : Substring) : Char

@[inline]

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

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

@[inline]

def Substring.drop : Substring → Nat → Substring

@[inline]

def Substring.dropRight : Substring → Nat → Substring

@[inline]

def Substring.take : Substring → Nat → Substring

@[inline]

def Substring.takeRight : Substring → Nat → Substring

@[inline]

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

@[inline]

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

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

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) : α

@[inline]

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

@[inline]

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

@[inline]

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

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

@[specialize #[]]

def Substring.takeWhileAux (s : String) (stopPos : 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.takeWhile : Substring → (Char → Bool) → Substring

@[inline]

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

@[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

@[inline]

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

@[inline]

def Substring.trimLeft (s : Substring) : Substring

@[inline]

def Substring.trimRight (s : Substring) : Substring

@[inline]

def Substring.trim : Substring → Substring

def Substring.isNat (s : Substring) : Bool

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

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

instance Substring.hasBeq : BEq Substring

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

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

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

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

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

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

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

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

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

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

def String.trimRight (s : String) : String

def String.trimLeft (s : String) : String

def String.trim (s : String) : String

@[inline]

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

@[inline]

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

def String.toUpper (s : String) : String

def String.toLower (s : String) : String

def String.capitalize (s : String) : String

def String.decapitalize (s : String) : String

def Char.toString (c : Char) : String