Legacy implementations of String operations

This file includes old definitions of String functions that were downstreamed from core to prevent Batteries.Data.String.Lemmas from breaking.

@[irreducible, specialize #[]]

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

Implementation of String.Legacy.map.

Equations

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

@[inline]

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

Applies the function f to every character in a string, returning a string that contains the resulting characters.

This is an old implementation, preserved here for users of the lemmas in Batteries.Data.String.Lemmas. Its runtime behavior is equivalent to that of String.map.

Examples:

• "abc123".map Char.toUpper = "ABC123"
• "".map Char.toUpper = ""

Equations

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

@[inline]

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

Removes the specified number of characters (Unicode code points) from the start of the string.

If n is greater than s.length, returns "".

This is an old implementation, preserved here for users of the lemmas in Batteries.Data.String.Lemmas. Its runtime behavior is equivalent to that of String.drop.

Examples:

• "red green blue".drop 4 = "green blue"
• "red green blue".drop 10 = "blue"
• "red green blue".drop 50 = ""

Equations

• String.Legacy.drop s n = (s.toRawSubstring.drop n).toString

@[inline]

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

Creates a new string that contains the first n characters (Unicode code points) of s.

If n is greater than s.length, returns s.

This is an old implementation, preserved here for users of the lemmas in Batteries.Data.String.Lemmas. Its runtime behavior is equivalent to that of String.take.

Examples:

• "red green blue".take 3 = "red"
• "red green blue".take 1 = "r"
• "red green blue".take 0 = ""
• "red green blue".take 100 = "red green blue"

Equations

• String.Legacy.take s n = (s.toRawSubstring.take n).toString

@[inline]

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

Creates a new string that contains the longest prefix of s in which p returns true for all characters.

This is an old implementation, preserved here for users of the lemmas in Batteries.Data.String.Lemmas. Its runtime behavior is equivalent to that of String.takeWhile.

Examples:

• "red green blue".takeWhile (·.isLetter) = "red"
• "red green blue".takeWhile (· == 'r') = "r"
• "red green blue".takeWhile (· != 'n') = "red gree"
• "red green blue".takeWhile (fun _ => true) = "red green blue"

Equations

• String.Legacy.takeWhile s p = (s.toRawSubstring.takeWhile p).toString

@[inline]

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

Creates a new string by removing the longest prefix from s in which p returns true for all characters.

This is an old implementation, preserved here for users of the lemmas in Batteries.Data.String.Lemmas. Its runtime behavior is equivalent to that of String.dropWhile.

Examples:

• "red green blue".dropWhile (·.isLetter) = " green blue"
• "red green blue".dropWhile (· == 'r') = "ed green blue"
• "red green blue".dropWhile (· != 'n') = "n blue"
• "red green blue".dropWhile (fun _ => true) = ""

Equations

• String.Legacy.dropWhile s p = (s.toRawSubstring.dropWhile p).toString

@[irreducible, specialize #[]]

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

Auxiliary definition for String.Legacy.foldl.

This is an old implementation, preserved here for users of the lemmas in Batteries.Data.String.Lemmas. Its runtime behavior is equivalent to that of String.foldlAux.

Equations

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

@[inline]

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

Folds a function over a string from the left, accumulating a value starting with init. The accumulated value is combined with each character in order, using f.

This is an old implementation, preserved here for users of the lemmas in Batteries.Data.String.Lemmas. Its runtime behavior is equivalent to that of String.foldl.

Examples:

• "coffee tea water".foldl (fun n c => if c.isWhitespace then n + 1 else n) 0 = 2
• "coffee tea and water".foldl (fun n c => if c.isWhitespace then n + 1 else n) 0 = 3
• "coffee tea water".foldl (·.push ·) "" = "coffee tea water"

Equations

• String.Legacy.foldl f init s = String.Legacy.foldlAux f s s.rawEndPos 0 init

@[inline]

def String.Legacy.front (s : String) : Char

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

This is an old implementation, preserved here for users of the lemmas in Batteries.Data.String.Lemmas. Its runtime behavior is equivalent to that of String.front.

Examples:

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

Equations

• String.Legacy.front s = String.Pos.Raw.get s 0

@[inline]

def String.Legacy.back (s : String) : Char

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

This is an old implementation, preserved here for users of the lemmas in Batteries.Data.String.Lemmas. Its runtime behavior is equivalent to that of String.back.

Examples:

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

Equations

• String.Legacy.back s = String.Pos.Raw.get s (String.Pos.Raw.prev s s.rawEndPos)

@[irreducible]

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

Auxuliary definition for String.Legacy.posOf.

This is an old implementation, preserved here for users of the lemmas in Batteries.Data.String.Lemmas.

Equations

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

@[inline]

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

Returns the position of the first occurrence of a character, c, in a string s. If s does not contain c, returns s.rawEndPos.

This is an old implementation, preserved here for users of the lemmas in Batteries.Data.String.Lemmas.

Examples:

• "abcba".posOf 'a' = ⟨0⟩
• "abcba".posOf 'z' = ⟨5⟩
• "L∃∀N".posOf '∀' = ⟨4⟩

Equations

• String.Legacy.posOf s c = String.Legacy.posOfAux s c s.rawEndPos 0

@[irreducible]

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

Auxuliary definition for String.Legacy.revPosOf.

This is an old implementation, preserved here for users of the lemmas in Batteries.Data.String.Lemmas.

Equations

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

@[inline]

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

Returns the position of the last occurrence of a character, c, in a string s. If s does not contain c, returns none.

This is an old implementation, preserved here for users of the lemmas in Batteries.Data.String.Lemmas.

Examples:

• "abcabc".revPosOf 'a' = some ⟨3⟩
• "abcabc".revPosOf 'z' = none
• "L∃∀N".revPosOf '∀' = some ⟨4⟩

Equations

• String.Legacy.revPosOf s c = String.Legacy.revPosOfAux s c s.rawEndPos

@[irreducible]

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

Auxuliary definition for String.Legacy.find.

This is an old implementation, preserved here for users of the lemmas in Batteries.Data.String.Lemmas.

Equations

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

@[inline]

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

Finds the position of the first character in a string for which the Boolean predicate p returns true. If there is no such character in the string, then the end position of the string is returned.

This is an old implementation, preserved here for users of the lemmas in Batteries.Data.String.Lemmas.

Examples:

• "coffee tea water".find (·.isWhitespace) = ⟨6⟩
• "tea".find (· == 'X') = ⟨3⟩
• "".find (· == 'X') = ⟨0⟩

Equations

• String.Legacy.find s p = String.Legacy.findAux s p s.rawEndPos 0

@[irreducible]

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

Auxuliary definition for String.Legacy.revFind.

This is an old implementation, preserved here for users of the lemmas in Batteries.Data.String.Lemmas.

Equations

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

@[inline]

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

Finds the position of the last character in a string for which the Boolean predicate p returns true. If there is no such character in the string, then none is returned.

This is an old implementation, preserved here for users of the lemmas in Batteries.Data.String.Lemmas.

Examples:

• "coffee tea water".revFind (·.isWhitespace) = some ⟨10⟩
• "tea".revFind (· == 'X') = none
• "".revFind (· == 'X') = none

Equations

• String.Legacy.revFind s p = String.Legacy.revFindAux s p s.rawEndPos

@[irreducible, specialize #[]]

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

Auxuliary definition for String.Legacy.foldr.

This is an old implementation, preserved here for users of the lemmas in Batteries.Data.String.Lemmas.

Equations

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

@[inline]

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

Folds a function over a string from the right, accumulating a value starting with init. The accumulated value is combined with each character in reverse order, using f.

This is an old implementation, preserved here for users of the lemmas in Batteries.Data.String.Lemmas.

Examples:

• "coffee tea water".foldr (fun c n => if c.isWhitespace then n + 1 else n) 0 = 2
• "coffee tea and water".foldr (fun c n => if c.isWhitespace then n + 1 else n) 0 = 3
• "coffee tea water".foldr (fun c s => c.push s) "" = "retaw dna aet eeffoc"

Equations

• String.Legacy.foldr f init s = String.Legacy.foldrAux f init s s.rawEndPos 0

@[irreducible, specialize #[]]

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

Auxuliary definition for String.Legacy.any.

This is an old implementation, preserved here for users of the lemmas in Batteries.Data.String.Lemmas.

Equations

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

@[inline]

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

Checks whether there is a character in a string for which the Boolean predicate p returns true.

Short-circuits at the first character for which p returns true.

This is an old implementation, preserved here for users of the lemmas in Batteries.Data.String.Lemmas.

Examples:

• "brown".any (·.isLetter) = true
• "brown".any (·.isWhitespace) = false
• "brown and orange".any (·.isLetter) = true
• "".any (fun _ => false) = false

Equations

• String.Legacy.any s p = String.Legacy.anyAux s s.rawEndPos p 0

@[inline]

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

Checks whether the Boolean predicate p returns true for every character in a string.

Short-circuits at the first character for which p returns false.

This is an old implementation, preserved here for users of the lemmas in Batteries.Data.String.Lemmas.

Examples:

• "brown".all (·.isLetter) = true
• "brown and orange".all (·.isLetter) = false
• "".all (fun _ => false) = true

Equations

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

@[inline]

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

Checks whether a string contains the specified character.

This is an old implementation, preserved here for users of the lemmas in Batteries.Data.String.Lemmas.

Examples:

• "green".contains 'e' = true
• "green".contains 'x' = false
• "".contains 'x' = false

Equations

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

@[inline]

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

Folds a function over a substring from the left, accumulating a value starting with init. The accumulated value is combined with each character in order, using f.

This is an old implementation, preserved here for users of the lemmas in Batteries.Data.String.Lemmas. Its runtime behavior is equivalent to that of Substring.Raw.foldl.

Equations

• Substring.Raw.Legacy.foldl f init { str := s_2, startPos := b, stopPos := e } = String.Legacy.foldlAux f s_2 e b init

@[inline]

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

Folds a function over a substring from the right, accumulating a value starting with init. The accumulated value is combined with each character in reverse order, using f.

This is an old implementation, preserved here for users of the lemmas in Batteries.Data.String.Lemmas.

Equations

• Substring.Raw.Legacy.foldr f init { str := s_2, startPos := b, stopPos := e } = String.Legacy.foldrAux f init s_2 e b

@[inline]

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

Checks whether the Boolean predicate p returns true for any character in a substring.

Short-circuits at the first character for which p returns true.

This is an old implementation, preserved here for users of the lemmas in Batteries.Data.String.Lemmas.

Equations

• Substring.Raw.Legacy.any { str := s_2, startPos := b, stopPos := e } p = String.Legacy.anyAux s_2 e p b

@[inline]

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

Checks whether the Boolean predicate p returns true for every character in a substring.

Short-circuits at the first character for which p returns false.

This is an old implementation, preserved here for users of the lemmas in Batteries.Data.String.Lemmas.

Equations

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

@[inline]

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

Checks whether a substring contains the specified character.

This is an old implementation, preserved here for users of the lemmas in Batteries.Data.String.Lemmas.

Equations

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