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

Equations

• List.asString s = { data := s }

instance String.instOfNatPos : OfNat String.Pos 0

Equations

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

instance String.instLTString : LT String

Equations

• String.instLTString = { 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

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

@[extern lean_string_length]

def String.length : String → Nat

Equations

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

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

Equations

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

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

Equations

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

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

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

Equations

• String.toList s = s.data

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.

Equations

• String.get s 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

Equations

• String.get? x✝ 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

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

Equations

• String.get! s 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

Equations

• String.set x✝¹ 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

Equations

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

@[extern lean_string_utf8_next]

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

Equations

• String.next s p = let c := String.get s 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

Equations

• String.prev x✝ 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

Equations

• String.front s = String.get s 0

def String.back (s : String) : Char

Equations

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

@[extern lean_string_utf8_at_end]

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

Equations

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

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

Equations

• String.get' s 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 : ¬String.atEnd s p = true) : String.Pos

Similar to next but runtime does not perform bounds check.

Equations

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

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

Equations

• String.posOf s c = String.posOfAux s c (String.endPos s) 0

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

Equations

• String.revPosOf s c = String.revPosOfAux s c (String.endPos s)

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

Equations

• String.find s p = String.findAux s p (String.endPos s) 0

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

Equations

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

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

Equations

• String.revFind s p = String.revFindAux s p (String.endPos s)

@[inline, reducible]

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

Equations

• String.Pos.min p₁ p₂ = { byteIdx := Nat.min p₁.byteIdx p₂.byteIdx }

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

Returns the first position where the two strings differ.

Equations

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

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

• String.extract x✝¹ 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

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

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

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

Equations

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

instance String.instInhabitedString : Inhabited String

Equations

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

instance String.instAppendString : Append String

Equations

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

def String.str : String → Char → String

Equations

• String.str = String.push

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

Equations

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

def String.isEmpty (s : String) : Bool

Equations

• String.isEmpty s = (String.endPos s == 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 = String.push "" c

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

Equations

• String.intercalate s 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

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

@[inline, reducible]

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) => String.utf8ByteSize i.s - i.i.byteIdx }

theorem String.Iterator.sizeOf_eq (i : String.Iterator) : sizeOf i = String.utf8ByteSize i.s - 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

• String.Iterator.remainingBytes x = match x with | { s := s, i := i } => (String.endPos s).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

• String.Iterator.curr x = match x with | { s := s, i := i } => String.get s 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

• String.Iterator.next x = match x with | { s := s, i := i } => { s := s, i := String.next s 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

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

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

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

Equations

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

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

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

Equations

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

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

True if the position is not zero.

Equations

• String.Iterator.hasPrev x = 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

• String.Iterator.setCurr x✝ x = match x✝, x with | { s := s, i := i }, c => { s := String.set s 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

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

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

• String.Iterator.extract x✝ x = match x✝, x with | { s := s₁, i := b }, { s := s₂, i := e } => if (decide (s₁ ≠ s₂) || decide (b > e)) = true then "" else String.extract s₁ 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

• 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

The remaining characters in an iterator, as a string.

Equations

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

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

• 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

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

• 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

Equations

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

@[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 (String.next s i) (f a (String.get s i)) else a

@[inline]

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

Equations

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

@[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 := String.prev s i; let a := f (String.get s 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 (String.endPos s) 0

@[specialize #[]]

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

Equations

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

@[inline]

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

Equations

• String.any s p = String.anyAux s (String.endPos s) p 0

@[inline]

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

Equations

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

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

Equations

• String.contains s c = String.any s 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 : (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

• String.mapAux f i s = if h : String.atEnd s i = true then s else let c := f (String.get s i); let_fun this := ⋯; let s := String.set s i c; String.mapAux f (String.next s 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

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

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

Equations

• String.toNat? s = if String.isNat s = true then some (String.foldl (fun (n : Nat) (c : Char) => n * 10 + (Char.toNat c - Char.toNat '0')) 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.

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

• String.isPrefixOf p s = String.substrEq p 0 s 0 (String.endPos p).byteIdx

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

Replace all occurrences of pattern in s with replacement.

Equations

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

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.

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

Return the beginning of the line that contains character pos.

Equations

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

@[inline]

def Substring.isEmpty (ss : Substring) : Bool

Equations

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

@[inline]

def Substring.toString : Substring → String

Equations

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

@[inline]

def Substring.toIterator : Substring → String.Iterator

Equations

• Substring.toIterator x = 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

• Substring.get x✝ x = match x✝, x with | { str := s, startPos := b, stopPos := stopPos }, p => String.get s (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

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

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.

Equations

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

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

Equations

• Substring.front s = Substring.get s 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

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

@[inline]

def Substring.drop : Substring → Nat → Substring

Equations

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

@[inline]

def Substring.dropRight : Substring → Nat → Substring

Equations

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

@[inline]

def Substring.take : Substring → Nat → Substring

Equations

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

@[inline]

def Substring.takeRight : Substring → Nat → Substring

Equations

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

@[inline]

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

Equations

• Substring.atEnd x✝ 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

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

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

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

@[inline]

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

Equations

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

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

Equations

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

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

Equations

• Substring.takeWhile x✝ 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

• Substring.dropWhile x✝ 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 }

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

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

@[inline]

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

Equations

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

@[inline]

def Substring.trimLeft (s : Substring) : Substring

Equations

• Substring.trimLeft s = Substring.dropWhile s Char.isWhitespace

@[inline]

def Substring.trimRight (s : Substring) : Substring

Equations

• Substring.trimRight s = Substring.dropRightWhile s 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

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

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

Equations

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

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

Equations

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

instance Substring.hasBeq : BEq Substring

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def String.trimRight (s : String) : String

Equations

• String.trimRight s = Substring.toString (Substring.trimRight (String.toSubstring s))

def String.trimLeft (s : String) : String

Equations

• String.trimLeft s = Substring.toString (Substring.trimLeft (String.toSubstring s))

def String.trim (s : String) : String

Equations

• String.trim s = Substring.toString (Substring.trim (String.toSubstring s))

@[inline]

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

Equations

• String.nextWhile s p i = Substring.takeWhileAux s (String.endPos s) p i

@[inline]

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

Equations

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

def String.toUpper (s : String) : String

Equations

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

def String.toLower (s : String) : String

Equations

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

def String.capitalize (s : String) : String

Equations

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

def String.decapitalize (s : String) : String

Equations

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

def Char.toString (c : Char) : String

Equations

• Char.toString c = String.singleton c