fix: Char -> Bool as default instance for string search (#11503)

This PR marks `Char -> Bool` patterns as default instances for string
search. This means that things like `" ".find (·.isWhitespace)` can now
be elaborated without error.

Previously, it was necessary to write `" ".find Char.isWhitespace`.

Thank you to David Christiansen for the idea of using a default
instance.

Author: TwoFX

src/Init/Data/String/Pattern/Pred.lean

@@ -79,9 +79,11 @@ instance : Std.Iterators.Finite (ForwardCharPredSearcher p s) Id :=
 instance : Std.Iterators.IteratorLoop (ForwardCharPredSearcher p s) Id Id :=
   .defaultImplementation
 
+@[default_instance]
 instance {p : Char → Bool} : ToForwardSearcher p (ForwardCharPredSearcher p) where
   toSearcher := iter p
 
+@[default_instance]
 instance {p : Char → Bool} : ForwardPattern p := .defaultImplementation
 
 instance {p : Char → Prop} [DecidablePred p] : ToForwardSearcher p (ForwardCharPredSearcher p) where
@@ -153,9 +155,11 @@ instance : Std.Iterators.Finite (BackwardCharPredSearcher s) Id :=
 instance : Std.Iterators.IteratorLoop (BackwardCharPredSearcher s) Id Id :=
   .defaultImplementation
 
+@[default_instance]
 instance {p : Char → Bool} : ToBackwardSearcher p BackwardCharPredSearcher where
   toSearcher := iter p
 
+@[default_instance]
 instance {p : Char → Bool} : BackwardPattern p := ToBackwardSearcher.defaultImplementation
 
 instance {p : Char → Prop} [DecidablePred p] : ToBackwardSearcher p BackwardCharPredSearcher where

src/Lean/Data/Xml/Parser.lean

@@ -154,7 +154,7 @@ def SystemLiteral : Parser String :=
 /-- https://www.w3.org/TR/xml/#NT-PubidChar -/
 def PubidChar : Parser LeanChar :=
   asciiLetter <|> digit <|> endl <|> attempt do
-  let c ← any
+  let c : _root_.Char := ← any
   if "-'()+,./:=?;!*#@$_%".contains c then pure c else fail "PublidChar expected"
 
 /-- https://www.w3.org/TR/xml/#NT-PubidLiteral -/

tests/lean/run/string_slice.lean

@@ -240,3 +240,12 @@ end
 
 #guard ("".toSlice.split "").toList == ["".toSlice, "".toSlice]
 #guard ("abc".toSlice.split "").toList == ["".toSlice, "a".toSlice, "b".toSlice, "c".toSlice, "".toSlice]
+
+#guard " ".find (·.isWhitespace) = " ".startPos
+#guard " ".find (· = ' ') = " ".startPos
+#guard " ".startsWith (·.isWhitespace) = true
+#guard " ".startsWith (· = ' ') = true
+#guard " ".revFind? (·.isWhitespace) = some " ".startPos
+#guard " ".revFind? (· = ' ') = some " ".startPos
+#guard " ".endsWith (·.isWhitespace) = true
+#guard " ".endsWith (· = ' ') = true