Skip to content

Commit cf0e444

Browse files
authored
chore: create alias String.Slice.any for String.Slice.contains (#11282)
This PR adds the alias `String.Slice.any` for `String.Slice.contains`. It would probably be even better to only have one, but we don't have a good mechanism for pointing people looking for one towards the other, so an alias it is for now.
1 parent 2c12bc9 commit cf0e444

File tree

1 file changed

+4
-0
lines changed

1 file changed

+4
-0
lines changed

src/Init/Data/String/Slice.lean

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -509,6 +509,10 @@ def contains [ToForwardSearcher ρ σ] (s : Slice) (pat : ρ) : Bool :=
509509
let searcher := ToForwardSearcher.toSearcher s pat
510510
searcher.any (· matches .matched ..)
511511

512+
@[inline, inherit_doc contains]
513+
def any [ToForwardSearcher ρ σ] (s : Slice) (pat : ρ) : Bool :=
514+
s.contains pat
515+
512516
/--
513517
Checks whether a slice only consists of matches of the pattern {name}`pat` anywhere.
514518

0 commit comments

Comments
 (0)