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

A step taken during the traversal of a Slice by a forward or backward searcher.

• rejected {s : Slice} (startPos endPos : s.Pos) : SearchStep s

  The subslice starting at startPos and ending at endPos did not match the pattern.

• matched {s : Slice} (startPos endPos : s.Pos) : SearchStep s

  The subslice starting at startPos and ending at endPos matches the pattern.

instance String.Slice.Pattern.instInhabitedSearchStep {a✝ : Slice} : Inhabited (SearchStep a✝)

def String.Slice.Pattern.instInhabitedSearchStep.default {a✝ : Slice} : SearchStep a✝

instance String.Slice.Pattern.instBEqSearchStep {s✝ : Slice} : BEq (SearchStep s✝)

def String.Slice.Pattern.instBEqSearchStep.beq {s✝ : Slice} : SearchStep s✝ → SearchStep s✝ → Bool

class String.Slice.Pattern.ToForwardSearcher {ρ : Type} (pat : ρ) (σ : outParam (Slice → Type)) : Type

Provides a conversion from a pattern to an iterator of SearchStep that searches for matches of the pattern from the start towards the end of a Slice.

• toSearcher (s : Slice) : Std.Iter (SearchStep s)

  Builds an iterator of SearchStep corresponding to matches of pat along the slice s. The SearchSteps returned by this iterator must contain ranges that are adjacent, non-overlapping and cover all of s.

class String.Slice.Pattern.ForwardPattern {ρ : Type} (pat : ρ) : Type

Provides simple pattern matching capabilities from the start of a Slice.

While these operations can be implemented on top of ToForwardSearcher some patterns allow for more efficient implementations. This class can be used to specialize for them. If there is no need to specialize in this fashion, then ForwardPattern.defaultImplementation can be used to automatically derive an instance.

• startsWith : Slice → Bool

  Checks whether the slice starts with the pattern.

• dropPrefix? (s : Slice) : Option s.Pos

  Checks whether the slice starts with the pattern. If it does, the slice is returned with the prefix removed; otherwise the result is none.

@[extern lean_string_memcmp]

def String.Slice.Pattern.Internal.memcmpStr (lhs rhs : String) (lstart rstart len : Pos.Raw) (h1 : len.offsetBy lstart ≤ lhs.rawEndPos) (h2 : len.offsetBy rstart ≤ rhs.rawEndPos) : Bool

@[inline]

def String.Slice.Pattern.Internal.memcmpSlice (lhs rhs : Slice) (lstart rstart len : Pos.Raw) (h1 : len.offsetBy lstart ≤ lhs.rawEndPos) (h2 : len.offsetBy rstart ≤ rhs.rawEndPos) : Bool

@[specialize #[3]]

def String.Slice.Pattern.ForwardPattern.defaultStartsWith {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (SearchStep s)] (pat : ρ) [ToForwardSearcher pat σ] (s : Slice) : Bool

@[specialize #[3]]

def String.Slice.Pattern.ForwardPattern.defaultDropPrefix? {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (SearchStep s)] (pat : ρ) [ToForwardSearcher pat σ] (s : Slice) : Option s.Pos

@[inline]

def String.Slice.Pattern.ForwardPattern.defaultImplementation {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (SearchStep s)] {pat : ρ} [ToForwardSearcher pat σ] : ForwardPattern pat

class String.Slice.Pattern.ToBackwardSearcher {ρ : Type} (pat : ρ) (σ : outParam (Slice → Type)) : Type

Provides a conversion from a pattern to an iterator of SearchStep searching for matches of the pattern from the end towards the start of a Slice.

• toSearcher (s : Slice) : Std.Iter (SearchStep s)

  Build an iterator of SearchStep corresponding to matches of pat along the slice s. The SearchSteps returned by this iterator must contain ranges that are adjacent, non-overlapping and cover all of s.

class String.Slice.Pattern.BackwardPattern {ρ : Type} (pat : ρ) : Type

Provides simple pattern matching capabilities from the end of a Slice.

While these operations can be implemented on top of ToBackwardSearcher, some patterns allow for more efficient implementations. This class can be used to specialize for them. If there is no need to specialize in this fashion, then BackwardPattern.defaultImplementation can be used to automatically derive an instance.

• endsWith : Slice → Bool

  Checks whether the slice ends with the pattern.

• dropSuffix? (s : Slice) : Option s.Pos

  Checks whether the slice ends with the pattern. If it does, the slice is returned with the suffix removed; otherwise the result is none.

@[specialize #[3]]

def String.Slice.Pattern.ToBackwardSearcher.defaultEndsWith {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (SearchStep s)] (pat : ρ) [ToBackwardSearcher pat σ] (s : Slice) : Bool

@[specialize #[3]]

def String.Slice.Pattern.ToBackwardSearcher.defaultDropSuffix? {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (SearchStep s)] (pat : ρ) [ToBackwardSearcher pat σ] (s : Slice) : Option s.Pos

@[inline]

def String.Slice.Pattern.ToBackwardSearcher.defaultImplementation {ρ : Type} {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (SearchStep s)] {pat : ρ} [ToBackwardSearcher pat σ] : BackwardPattern pat