Documentation

Init.Data.String.Pattern.String

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.

Instances For

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

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

Instances For

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

ForwardSliceSearcher a✝

Equations

String.Slice.Pattern.ForwardSliceSearcher.instInhabited.default = String.Slice.Pattern.ForwardSliceSearcher.emptyBefore default

Instances For

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 (s pat : Slice) :

Std.Iter (SearchStep s)

Equations

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

Instances For

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.

instance String.Slice.Pattern.ForwardSliceSearcher.instFiniteIdSearchStep {s : Slice} :

Std.Iterators.Finite (ForwardSliceSearcher s) Id

instance String.Slice.Pattern.ForwardSliceSearcher.instIteratorCollectIdSearchStep {s : Slice} :

Std.Iterators.IteratorCollect (ForwardSliceSearcher s) Id Id

Equations

String.Slice.Pattern.ForwardSliceSearcher.instIteratorCollectIdSearchStep = Std.Iterators.IteratorCollect.defaultImplementation

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

Equations

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

Instances For

@[inline]

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

Equations

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

Instances For

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

Equations

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

Instances For

@[inline]

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

Equations

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

Instances For

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.