This module defines the necessary instances to register String and String.Slice with the pattern framework.

def String.Slice.Pattern.ForwardSliceSearcher.buildTable (pat : Slice) : Vector Nat pat.utf8ByteSize

theorem String.Slice.Pattern.ForwardSliceSearcher.getElem_buildTable_le (pat : Slice) (i : Nat) (hi : i < pat.utf8ByteSize) : (buildTable pat)[i] ≤ i

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

• emptyBefore {s : Slice} (pos : s.Pos) : ForwardSliceSearcher s
• emptyAt {s : Slice} (pos : s.Pos) (h : pos ≠ s.endPos) : ForwardSliceSearcher s
• proper {s : Slice} (needle : Slice) (table : Vector Nat needle.utf8ByteSize) (ht : table = buildTable needle) (stackPos needlePos : Pos.Raw) (hn : needlePos < needle.rawEndPos) : ForwardSliceSearcher s
• atEnd {s : Slice} : ForwardSliceSearcher s

@[instance_reducible]

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

@[inline]

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

@[instance_reducible]

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

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

@[instance_reducible]

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

@[instance_reducible]

instance String.Slice.Pattern.ForwardSliceSearcher.instToForwardSearcher {pat : Slice} : ToForwardSearcher pat ForwardSliceSearcher

@[inline]

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

@[inline]

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

@[instance_reducible]

instance String.Slice.Pattern.ForwardSliceSearcher.instForwardPattern {pat : Slice} : ForwardPattern pat

@[instance_reducible]

instance String.Slice.Pattern.ForwardSliceSearcher.instToForwardSearcher_1 {pat : String} : ToForwardSearcher pat ForwardSliceSearcher

@[instance_reducible]

instance String.Slice.Pattern.ForwardSliceSearcher.instForwardPattern_1 {pat : String} : ForwardPattern pat

@[inline]

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

@[inline]

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

@[instance_reducible]

instance String.Slice.Pattern.BackwardSliceSearcher.instBackwardPattern {pat : Slice} : BackwardPattern pat

@[instance_reducible]

instance String.Slice.Pattern.BackwardSliceSearcher.instBackwardPattern_1 {pat : String} : BackwardPattern pat