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

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

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 for String. That is, a String and a position in that string.

• s : String
• i : String.Pos

instance String.instDecidableEqIterator : DecidableEq String.Iterator

Equations

• String.instDecidableEqIterator = String.decEqIterator✝

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

Equations

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

@[inline, reducible]

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

Equations

• String.iter = String.mkIterator

instance String.instSizeOfIterator : SizeOf String.Iterator

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 : String.Iterator → String

Equations

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

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

Equations

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

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

Equations

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

def String.Iterator.curr : String.Iterator → 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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[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 (Char.ofNat 48))) 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

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

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

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 (Char.ofNat 48))) 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