inductive String.Slice.Pattern.ForwardSliceSearcher (s : Slice) : Type

• empty {s : Slice} (pos : s.Pos) : ForwardSliceSearcher s
• proper {s : Slice} (needle : Slice) (table : Array Pos.Raw) (stackPos needlePos : Pos.Raw) : ForwardSliceSearcher s
• atEnd {s : Slice} : ForwardSliceSearcher s

instance String.Slice.Pattern.instInhabitedForwardSliceSearcher {a✝ : Slice} : Inhabited (ForwardSliceSearcher a✝)

Equations

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

def String.Slice.Pattern.instInhabitedForwardSliceSearcher.default {a✝ : Slice} : ForwardSliceSearcher a✝

Equations

• String.Slice.Pattern.instInhabitedForwardSliceSearcher.default = String.Slice.Pattern.ForwardSliceSearcher.empty default

def String.Slice.Pattern.ForwardSliceSearcher.buildTable (pat : Slice) : Array Pos.Raw

Equations

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

@[inline]

def String.Slice.Pattern.ForwardSliceSearcher.iter (s pat : Slice) : Std.Iter (SearchStep s)

Equations

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

partial def String.Slice.Pattern.ForwardSliceSearcher.backtrackIfNecessary (pat : Slice) (table : Array Pos.Raw) (stackByte : UInt8) (needlePos : Pos.Raw) : Pos.Raw

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

Equations

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

@[irreducible]

def String.Slice.Pattern.ForwardSliceSearcher.instIteratorIdSearchStep.findNext (s needle : Slice) (table : Array Pos.Raw) (stackPos needlePos startPos currStackPos needlePos✝ : Pos.Raw) (h : stackPos ≤ currStackPos) : Id (Std.Shrink (Std.Iterators.PlausibleIterStep fun (x : Std.Iterators.IterStep (Std.IterM Id (SearchStep s)) (SearchStep s)) => match x with | Std.Iterators.IterStep.yield it' out => match { internalState := proper needle table stackPos needlePos }.internalState with | empty pos => (∃ (newPos : s.Pos), pos < newPos ∧ it'.internalState = empty newPos) ∨ it'.internalState = atEnd | proper needle table stackPos needlePos => (∃ (newStackPos : Pos.Raw), ∃ (newNeedlePos : Pos.Raw), stackPos < newStackPos ∧ newStackPos ≤ s.rawEndPos ∧ it'.internalState = proper needle table newStackPos newNeedlePos) ∨ it'.internalState = atEnd | atEnd => False | Std.Iterators.IterStep.skip it => False | Std.Iterators.IterStep.done => True))

Equations

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

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

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

Equations

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

instance String.Slice.Pattern.ForwardSliceSearcher.instToForwardSearcher : ToForwardSearcher Slice ForwardSliceSearcher

Equations

• String.Slice.Pattern.ForwardSliceSearcher.instToForwardSearcher = { toSearcher := String.Slice.Pattern.ForwardSliceSearcher.iter }

@[inline]

def String.Slice.Pattern.ForwardSliceSearcher.startsWith (s pat : Slice) : Bool

Equations

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

@[inline]

def String.Slice.Pattern.ForwardSliceSearcher.dropPrefix? (s pat : Slice) : Option s.Pos

Equations

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

instance String.Slice.Pattern.ForwardSliceSearcher.instForwardPattern : ForwardPattern Slice

Equations

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

instance String.Slice.Pattern.ForwardSliceSearcher.instToForwardSearcher_1 : ToForwardSearcher String ForwardSliceSearcher

Equations

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

instance String.Slice.Pattern.ForwardSliceSearcher.instForwardPattern_1 : ForwardPattern String

Equations

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

@[inline]

def String.Slice.Pattern.BackwardSliceSearcher.endsWith (s pat : Slice) : Bool

Equations

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

@[inline]

def String.Slice.Pattern.BackwardSliceSearcher.dropSuffix? (s pat : Slice) : Option s.Pos

Equations

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

instance String.Slice.Pattern.BackwardSliceSearcher.instBackwardPattern : BackwardPattern Slice

Equations

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

instance String.Slice.Pattern.BackwardSliceSearcher.instBackwardPattern_1 : BackwardPattern String

Equations

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