structure String.Slice.Pattern.ForwardCharSearcher (needle : Char) (s : Slice) : Type

• currPos : s.Pos

def String.Slice.Pattern.instInhabitedForwardCharSearcher.default {a✝ : Char} {a✝¹ : Slice} : ForwardCharSearcher a✝ a✝¹

Equations

• String.Slice.Pattern.instInhabitedForwardCharSearcher.default = { currPos := default }

instance String.Slice.Pattern.instInhabitedForwardCharSearcher {a✝ : Char} {a✝¹ : Slice} : Inhabited (ForwardCharSearcher a✝ a✝¹)

Equations

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

@[inline]

def String.Slice.Pattern.ForwardCharSearcher.iter (c : Char) (s : Slice) : Std.Iter (SearchStep s)

Equations

• String.Slice.Pattern.ForwardCharSearcher.iter c s = { internalState := { currPos := s.startPos } }

instance String.Slice.Pattern.ForwardCharSearcher.instIteratorIdSearchStep {c : Char} (s : Slice) : Std.Iterator (ForwardCharSearcher c s) Id (SearchStep s)

Equations

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

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

Equations

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

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

instance String.Slice.Pattern.ForwardCharSearcher.instIteratorLoopIdSearchStep {s : Char} {c : Slice} : Std.IteratorLoop (ForwardCharSearcher s c) Id Id

Equations

• String.Slice.Pattern.ForwardCharSearcher.instIteratorLoopIdSearchStep = Std.IteratorLoop.defaultImplementation

instance String.Slice.Pattern.ForwardCharSearcher.instToForwardSearcherChar {c : Char} : ToForwardSearcher c (ForwardCharSearcher c)

Equations

• String.Slice.Pattern.ForwardCharSearcher.instToForwardSearcherChar = { toSearcher := String.Slice.Pattern.ForwardCharSearcher.iter c }

instance String.Slice.Pattern.ForwardCharSearcher.instForwardPatternChar {c : Char} : ForwardPattern c

Equations

• String.Slice.Pattern.ForwardCharSearcher.instForwardPatternChar = String.Slice.Pattern.ForwardPattern.defaultImplementation

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

• currPos : s.Pos
• needle : Char

instance String.Slice.Pattern.instInhabitedBackwardCharSearcher {a✝ : Slice} : Inhabited (BackwardCharSearcher a✝)

Equations

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

def String.Slice.Pattern.instInhabitedBackwardCharSearcher.default {a✝ : Slice} : BackwardCharSearcher a✝

Equations

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

@[inline]

def String.Slice.Pattern.BackwardCharSearcher.iter (c : Char) (s : Slice) : Std.Iter (SearchStep s)

Equations

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

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

Equations

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

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

Equations

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

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

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

Equations

• String.Slice.Pattern.BackwardCharSearcher.instIteratorLoopIdSearchStep = Std.IteratorLoop.defaultImplementation

instance String.Slice.Pattern.BackwardCharSearcher.instToBackwardSearcherChar {c : Char} : ToBackwardSearcher c BackwardCharSearcher

Equations

• String.Slice.Pattern.BackwardCharSearcher.instToBackwardSearcherChar = { toSearcher := String.Slice.Pattern.BackwardCharSearcher.iter c }

instance String.Slice.Pattern.BackwardCharSearcher.instBackwardPatternChar {c : Char} : BackwardPattern c

Equations

• String.Slice.Pattern.BackwardCharSearcher.instBackwardPatternChar = String.Slice.Pattern.ToBackwardSearcher.defaultImplementation