Skip to content

Commit 8293352

Browse files
committed
Use Iter.findSome?
1 parent 5c2d236 commit 8293352

File tree

1 file changed

+2
-6
lines changed

1 file changed

+2
-6
lines changed

src/Init/Data/String/Slice.lean

Lines changed: 2 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -462,9 +462,7 @@ Examples:
462462
@[specialize pat]
463463
def find? [ToForwardSearcher ρ σ] (s : Slice) (pat : ρ) : Option s.Pos :=
464464
let searcher := ToForwardSearcher.toSearcher s pat
465-
match Internal.nextMatch searcher with
466-
| some (_, startPos, _) => some startPos
467-
| none => none
465+
searcher.findSome? (fun | .matched startPos _ => some startPos | .rejected .. => none)
468466

469467
/--
470468
Checks whether a slice has a match of the pattern {name}`pat` anywhere.
@@ -774,9 +772,7 @@ Examples:
774772
@[specialize pat]
775773
def revFind? [ToBackwardSearcher ρ σ] (s : Slice) (pat : ρ) : Option s.Pos :=
776774
let searcher := ToBackwardSearcher.toSearcher s pat
777-
match Internal.nextMatch searcher with
778-
| some (_, startPos, _) => some startPos
779-
| none => none
775+
searcher.findSome? (fun | .matched startPos _ => some startPos | .rejected .. => none)
780776

781777
end BackwardPatternUsers
782778

0 commit comments

Comments
 (0)