@[instance_reducible]

instance String.Slice.Pattern.Model.CharPred.instForwardPatternModelForallCharBool {p : Char → Bool} : ForwardPatternModel p

Equations

• String.Slice.Pattern.Model.CharPred.instForwardPatternModelForallCharBool = { Matches := fun (s : String) => ∃ (c : Char), s = String.singleton c ∧ p c = true, not_matches_empty := ⋯ }

instance String.Slice.Pattern.Model.CharPred.instNoPrefixForwardPatternModelForallCharBool {p : Char → Bool} : NoPrefixForwardPatternModel p

theorem String.Slice.Pattern.Model.CharPred.isMatch_iff {p : Char → Bool} {s : Slice} {pos : s.Pos} : IsMatch p pos ↔ ∃ (h : s.startPos ≠ s.endPos), pos = s.startPos.next h ∧ p (s.startPos.get h) = true

theorem String.Slice.Pattern.Model.CharPred.isLongestMatch_iff {p : Char → Bool} {s : Slice} {pos : s.Pos} : IsLongestMatch p pos ↔ ∃ (h : s.startPos ≠ s.endPos), pos = s.startPos.next h ∧ p (s.startPos.get h) = true

instance String.Slice.Pattern.Model.CharPred.instLawfulForwardPatternModelForallCharBool {p : Char → Bool} : LawfulForwardPatternModel p

instance String.Slice.Pattern.Model.CharPred.instLawfulToForwardSearcherModelForallCharBoolDefaultForwardSearcher {p : Char → Bool} : LawfulToForwardSearcherModel p

@[instance_reducible]

instance String.Slice.Pattern.Model.CharPred.Decidable.instForwardPatternModelForallCharPropOfDecidablePred {p : Char → Prop} [DecidablePred p] : ForwardPatternModel p

Equations

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

instance String.Slice.Pattern.Model.CharPred.Decidable.instNoPrefixForwardPatternModelForallCharProp {p : Char → Prop} [DecidablePred p] : NoPrefixForwardPatternModel p

theorem String.Slice.Pattern.Model.CharPred.Decidable.isMatch_iff_isMatch_decide {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} : IsMatch p pos ↔ IsMatch (fun (x : Char) => decide (p x)) pos

theorem String.Slice.Pattern.Model.CharPred.Decidable.isMatch_iff {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} : IsMatch p pos ↔ ∃ (h : s.startPos ≠ s.endPos), pos = s.startPos.next h ∧ p (s.startPos.get h)

theorem String.Slice.Pattern.Model.CharPred.Decidable.isLongestMatch_iff {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} : IsLongestMatch p pos ↔ ∃ (h : s.startPos ≠ s.endPos), pos = s.startPos.next h ∧ p (s.startPos.get h)

theorem String.Slice.Pattern.Model.CharPred.Decidable.isLongestMatch_iff_isLongestMatch_decide {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} : IsLongestMatch p pos ↔ IsLongestMatch (fun (x : Char) => decide (p x)) pos

theorem String.Slice.Pattern.Model.CharPred.Decidable.dropPrefix?_eq_dropPrefix?_decide {p : Char → Prop} [DecidablePred p] : ForwardPattern.dropPrefix? p = ForwardPattern.dropPrefix? fun (x : Char) => decide (p x)

instance String.Slice.Pattern.Model.CharPred.Decidable.instLawfulForwardPatternModelForallCharProp {p : Char → Prop} [DecidablePred p] : LawfulForwardPatternModel p

instance String.Slice.Pattern.Model.CharPred.Decidable.instLawfulToForwardSearcherModelForallCharPropDefaultForwardSearcher {p : Char → Prop} [DecidablePred p] : LawfulToForwardSearcherModel p