@[instance_reducible]

instance String.Slice.Pattern.Model.Char.instForwardPatternModelChar {c : Char} : ForwardPatternModel c

Equations

• String.Slice.Pattern.Model.Char.instForwardPatternModelChar = { Matches := fun (s : String) => s = String.singleton c, not_matches_empty := ⋯ }

instance String.Slice.Pattern.Model.Char.instNoPrefixForwardPatternModelChar {c : Char} : NoPrefixForwardPatternModel c

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

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

instance String.Slice.Pattern.Model.Char.instLawfulForwardPatternModelChar {c : Char} : LawfulForwardPatternModel c

instance String.Slice.Pattern.Model.Char.instLawfulToForwardSearcherModelCharDefaultForwardSearcher {c : Char} : LawfulToForwardSearcherModel c