@[inline]

def String.replace {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (Slice.Pattern.SearchStep s)] [∀ (s : Slice), Std.Iterators.Finite (σ s) Id] [(s : Slice) → Std.Iterators.IteratorLoop (σ s) Id Id] {α : Type u_1} [Slice.Pattern.ToForwardSearcher ρ σ] [ToSlice α] (s : String) (pattern : ρ) (replacement : α) : String

Constructs a new string obtained by replacing all occurrences of pattern with replacement in s.

This function is generic over all currently supported patterns. The replacement may be a String or a String.Slice.

Examples:

• "red green blue".replace 'e' "" = "rd grn blu"

• "red green blue".replace (fun c => c == 'u' || c == 'e') "" = "rd grn bl"

• "red green blue".replace "e" "" = "rd grn blu"

• "red green blue".replace "ee" "E" = "red grEn blue"

• "red green blue".replace "e" "E" = "rEd grEEn bluE"

• "aaaaa".replace "aa" "b" = "bba"

• "abc".replace "" "k" = "kakbkck"

Equations

• s.replace pattern replacement = s.toSlice.replace pattern replacement

@[inline]

def String.Slice.Pos.find? {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (Pattern.SearchStep s)] [∀ (s : Slice), Std.Iterators.Finite (σ s) Id] [(s : Slice) → Std.Iterators.IteratorLoop (σ s) Id Id] [Pattern.ToForwardSearcher ρ σ] {s : Slice} (pos : s.Pos) (pattern : ρ) : Option s.Pos

Finds the position of the first match of the pattern pattern in after the position pos. If there is no match none is returned.

This function is generic over all currently supported patterns.

Examples:

• ("coffee tea water".toSlice.startPos.find? Char.isWhitespace).map (·.get!) == some ' '

• ("tea".toSlice.pos ⟨1⟩ (by decide)).find? (fun (c : Char) => c == 't') == none

Equations

• pos.find? pattern = Option.map String.Slice.Pos.ofReplaceStart ((s.replaceStart pos).find? pattern)

@[inline]

def String.ValidPos.find? {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (Slice.Pattern.SearchStep s)] [∀ (s : Slice), Std.Iterators.Finite (σ s) Id] [(s : Slice) → Std.Iterators.IteratorLoop (σ s) Id Id] [Slice.Pattern.ToForwardSearcher ρ σ] {s : String} (pos : s.ValidPos) (pattern : ρ) : Option s.ValidPos

Finds the position of the first match of the pattern pattern in after the position pos. If there is no match none is returned.

This function is generic over all currently supported patterns.

Examples:

• ("coffee tea water".startValidPos.find? Char.isWhitespace).map (·.get!) == some ' '

• ("tea".pos ⟨1⟩ (by decide)).find? (fun (c : Char) => c == 't') == none

Equations

• pos.find? pattern = Option.map (fun (x : s.toSlice.Pos) => x.ofSlice) (pos.toSlice.find? pattern)

@[inline]

def String.find? {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterators.Iterator (σ s) Id (Slice.Pattern.SearchStep s)] [∀ (s : Slice), Std.Iterators.Finite (σ s) Id] [(s : Slice) → Std.Iterators.IteratorLoop (σ s) Id Id] [Slice.Pattern.ToForwardSearcher ρ σ] (s : String) (pattern : ρ) : Option s.ValidPos

Finds the position of the first match of the pattern pattern in a string s. If there is no match none is returned.

This function is generic over all currently supported patterns.

Examples:

• ("coffee tea water".find? Char.isWhitespace).map (·.get!) == some ' '

• "tea".find? (fun (c : Char) => c == 'X') == none

• ("coffee tea water".find? "tea").map (·.get!) == some 't'

Equations

• s.find? pattern = s.startValidPos.find? pattern