structure String.Slice.Pattern.ForwardCharPredSearcher (p : Char → Bool) (s : Slice) : Type

• currPos : s.Pos

instance String.Slice.Pattern.instInhabitedForwardCharPredSearcher {a✝ : Char → Bool} {a✝¹ : Slice} : Inhabited (ForwardCharPredSearcher a✝ a✝¹)

Equations

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

def String.Slice.Pattern.instInhabitedForwardCharPredSearcher.default {a✝ : Char → Bool} {a✝¹ : Slice} : ForwardCharPredSearcher a✝ a✝¹

Equations

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

@[inline]

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

Equations

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

instance String.Slice.Pattern.ForwardCharPredSearcher.instIteratorIdSearchStep {p : Char → Bool} (s : Slice) : Std.Iterators.Iterator (ForwardCharPredSearcher p s) Id (SearchStep s)

Equations

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

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

Equations

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

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

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

Equations

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

@[defaultInstance 1000]

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

Equations

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

@[defaultInstance 1000]

instance String.Slice.Pattern.ForwardCharPredSearcher.instForwardPatternForallCharBool {p : Char → Bool} : ForwardPattern p

Equations

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

instance String.Slice.Pattern.ForwardCharPredSearcher.instToForwardSearcherForallCharPropDecide {p : Char → Prop} [DecidablePred p] : ToForwardSearcher p (ForwardCharPredSearcher fun (b : Char) => decide (p b))

Equations

• String.Slice.Pattern.ForwardCharPredSearcher.instToForwardSearcherForallCharPropDecide = { toSearcher := String.Slice.Pattern.ForwardCharPredSearcher.iter fun (x : Char) => decide (p x) }

instance String.Slice.Pattern.ForwardCharPredSearcher.instForwardPatternForallCharPropOfDecidablePred {p : Char → Prop} [DecidablePred p] : ForwardPattern p

Equations

• String.Slice.Pattern.ForwardCharPredSearcher.instForwardPatternForallCharPropOfDecidablePred = 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 (c : Char → Bool) (s : Slice) : Std.Iter (SearchStep s)

Equations

• String.Slice.Pattern.BackwardCharPredSearcher.iter c s = { 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

@[defaultInstance 1000]

instance String.Slice.Pattern.BackwardCharPredSearcher.instToBackwardSearcherForallCharBool {p : Char → Bool} : ToBackwardSearcher p BackwardCharPredSearcher

Equations

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

@[defaultInstance 1000]

instance String.Slice.Pattern.BackwardCharPredSearcher.instBackwardPatternForallCharBool {p : Char → Bool} : BackwardPattern p

Equations

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

instance String.Slice.Pattern.BackwardCharPredSearcher.instToBackwardSearcherForallCharPropOfDecidablePred {p : Char → Prop} [DecidablePred p] : ToBackwardSearcher p BackwardCharPredSearcher

Equations

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

instance String.Slice.Pattern.BackwardCharPredSearcher.instBackwardPatternForallCharPropOfDecidablePred {p : Char → Prop} [DecidablePred p] : BackwardPattern p

Equations

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