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₂ => 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

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

@[inline]

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

Equations

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

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

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

Equations

• String.revPosOf s c = if (String.endPos s == 0) = true then none else String.revPosOfAux s c (String.prev s (String.endPos s))

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

@[inline]

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

Equations

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

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

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

Equations

• String.revFind s p = if (String.endPos s == 0) = true then none else String.revFindAux s p (String.prev s (String.endPos s))

@[inline]

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

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

@[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 { data := [] } 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 #[]]

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

@[specialize #[]]

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

Equations

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

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

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

• s : String
• i : String.Pos

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

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]

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

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

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 = String.foldlAux.loop f s stopPos i a

partial def String.foldlAux.loop {α : Type u} (f : α → Char → α) (s : String) (stopPos : String.Pos) (i : String.Pos) (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) (stopPos : String.Pos) (i : String.Pos) : α

Equations

• String.foldrAux f a s stopPos i = String.foldrAux.loop f a s stopPos i

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

@[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 = String.anyAux.loop s stopPos p i

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

@[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 => !p c

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

Equations

• String.contains s c = String.any s fun a => a == c

@[specialize #[]]

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

@[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.isDigit x)

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

Equations

• String.toNat? s = if String.isNat s = true then some (String.foldl (fun n c => 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.

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

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

Equations

• String.replace s pattern replacement = String.replace.loop s pattern replacement "" 0 0

partial def String.replace.loop (s : String) (pattern : String) (replacement : String) (acc : String) (accStop : String.Pos) (pos : String.Pos) : String

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

• Substring.next x x = match x, x with | { str := s, startPos := b, stopPos := e }, p => let absP := b + p; if absP = e then p else { byteIdx := (String.next s absP).byteIdx - b.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 occurence 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 []

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

@[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 => !p c

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

Equations

• Substring.contains s c = Substring.any s fun a => a == c

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

@[inline]

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

Equations

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

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

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

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

Equations

• Substring.toNat? s = if Substring.isNat s = true then some (Substring.foldl (fun n c => 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 => !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