From cf0e4441e898b753bff6a70320e2d072f0886b22 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Thu, 20 Nov 2025 14:21:30 +0100
Subject: [PATCH] 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.
---
 src/Init/Data/String/Slice.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/Init/Data/String/Slice.lean b/src/Init/Data/String/Slice.lean
index bc2c2711a4..8bba6c0a3e 100644
--- a/src/Init/Data/String/Slice.lean
+++ b/src/Init/Data/String/Slice.lean
@@ -509,6 +509,10 @@ def contains [ToForwardSearcher ρ σ] (s : Slice) (pat : ρ) : Bool :=
   let searcher := ToForwardSearcher.toSearcher s pat
   searcher.any (· matches .matched ..)
 
+@[inline, inherit_doc contains]
+def any [ToForwardSearcher ρ σ] (s : Slice) (pat : ρ) : Bool :=
+  s.contains pat
+
 /--
 Checks whether a slice only consists of matches of the pattern {name}`pat` anywhere.