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

Equations

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

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✝)

Equations

• String.Slice.Pattern.ForwardSliceSearcher.instInhabited = { default := String.Slice.Pattern.ForwardSliceSearcher.instInhabited.default }

@[inline]

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

Equations

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

@[instance_reducible]

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

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_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

• String.Slice.Pattern.ForwardSliceSearcher.instToForwardSearcher_1 = { toSearcher := String.Slice.Pattern.ForwardSliceSearcher.iter pat.toSlice }

@[instance_reducible]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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