structure String.Slice.Pattern.ForwardCharPredSearcher (s : Slice) : Type

• currPos : s.Pos
• needle : Char → Bool

instance String.Slice.Pattern.instInhabitedForwardCharPredSearcher {a✝ : Slice} : Inhabited (ForwardCharPredSearcher a✝)

Equations

• String.Slice.Pattern.instInhabitedForwardCharPredSearcher = { default := String.Slice.Pattern.instInhabitedForwardCharPredSearcher.default }

def String.Slice.Pattern.instInhabitedForwardCharPredSearcher.default {a✝ : Slice} : ForwardCharPredSearcher a✝

Equations

• String.Slice.Pattern.instInhabitedForwardCharPredSearcher.default = { currPos := default, needle := default }

@[inline]

def String.Slice.Pattern.ForwardCharPredSearcher.iter (s : Slice) (p : Char → Bool) : Std.Iter (SearchStep s)

Equations

• String.Slice.Pattern.ForwardCharPredSearcher.iter s p = { internalState := { currPos := s.startPos, needle := p } }

instance String.Slice.Pattern.ForwardCharPredSearcher.instIteratorIdSearchStep (s : Slice) : Std.Iterators.Iterator (ForwardCharPredSearcher s) Id (SearchStep s)

Equations

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

def String.Slice.Pattern.ForwardCharPredSearcher.finitenessRelation {s : Slice} : Std.Iterators.FinitenessRelation (ForwardCharPredSearcher s) Id

Equations

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

instance String.Slice.Pattern.ForwardCharPredSearcher.instFiniteIdSearchStep {s : Slice} : Std.Iterators.Finite (ForwardCharPredSearcher s) Id

instance String.Slice.Pattern.ForwardCharPredSearcher.instIteratorLoopIdSearchStep {s : Slice} : Std.Iterators.IteratorLoop (ForwardCharPredSearcher s) Id Id

Equations

• String.Slice.Pattern.ForwardCharPredSearcher.instIteratorLoopIdSearchStep = Std.Iterators.IteratorLoop.defaultImplementation

instance String.Slice.Pattern.ForwardCharPredSearcher.instToForwardSearcherForallCharBool : ToForwardSearcher (Char → Bool) ForwardCharPredSearcher

Equations

• String.Slice.Pattern.ForwardCharPredSearcher.instToForwardSearcherForallCharBool = { toSearcher := String.Slice.Pattern.ForwardCharPredSearcher.iter }

instance String.Slice.Pattern.ForwardCharPredSearcher.instForwardPatternForallCharBool : ForwardPattern (Char → Bool)

Equations

• String.Slice.Pattern.ForwardCharPredSearcher.instForwardPatternForallCharBool = String.Slice.Pattern.ForwardPattern.defaultImplementation

structure String.Slice.Pattern.BackwardCharPredSearcher (s : Slice) : Type

• currPos : s.Pos
• needle : Char → Bool

def String.Slice.Pattern.instInhabitedBackwardCharPredSearcher.default {a✝ : Slice} : BackwardCharPredSearcher a✝

Equations

• String.Slice.Pattern.instInhabitedBackwardCharPredSearcher.default = { currPos := default, needle := default }

instance String.Slice.Pattern.instInhabitedBackwardCharPredSearcher {a✝ : Slice} : Inhabited (BackwardCharPredSearcher a✝)

Equations

• String.Slice.Pattern.instInhabitedBackwardCharPredSearcher = { default := String.Slice.Pattern.instInhabitedBackwardCharPredSearcher.default }

@[inline]

def String.Slice.Pattern.BackwardCharPredSearcher.iter (s : Slice) (c : Char → Bool) : Std.Iter (SearchStep s)

Equations

• String.Slice.Pattern.BackwardCharPredSearcher.iter s c = { internalState := { currPos := s.endPos, needle := c } }

instance String.Slice.Pattern.BackwardCharPredSearcher.instIteratorIdSearchStep (s : Slice) : Std.Iterators.Iterator (BackwardCharPredSearcher s) Id (SearchStep s)

Equations

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

def String.Slice.Pattern.BackwardCharPredSearcher.finitenessRelation {s : Slice} : Std.Iterators.FinitenessRelation (BackwardCharPredSearcher s) Id

Equations

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

instance String.Slice.Pattern.BackwardCharPredSearcher.instFiniteIdSearchStep {s : Slice} : Std.Iterators.Finite (BackwardCharPredSearcher s) Id

instance String.Slice.Pattern.BackwardCharPredSearcher.instIteratorLoopIdSearchStep {s : Slice} : Std.Iterators.IteratorLoop (BackwardCharPredSearcher s) Id Id

Equations

• String.Slice.Pattern.BackwardCharPredSearcher.instIteratorLoopIdSearchStep = Std.Iterators.IteratorLoop.defaultImplementation

instance String.Slice.Pattern.BackwardCharPredSearcher.instToBackwardSearcherForallCharBool : ToBackwardSearcher (Char → Bool) BackwardCharPredSearcher

Equations

• String.Slice.Pattern.BackwardCharPredSearcher.instToBackwardSearcherForallCharBool = { toSearcher := String.Slice.Pattern.BackwardCharPredSearcher.iter }

instance String.Slice.Pattern.BackwardCharPredSearcher.instBackwardPatternForallCharBool : BackwardPattern (Char → Bool)

Equations

• String.Slice.Pattern.BackwardCharPredSearcher.instBackwardPatternForallCharBool = String.Slice.Pattern.ToBackwardSearcher.defaultImplementation