feat: add grind_pattern command (#6470)

This PR introduces a command for specifying patterns used in the
heuristic instantiation of global theorems in the `grind` tactic. Note
that this PR only adds the parser.

src/Lean/Meta/Tactic/Grind.lean

@@ -20,6 +20,7 @@ import Lean.Meta.Tactic.Grind.Propagate
 import Lean.Meta.Tactic.Grind.PP
 import Lean.Meta.Tactic.Grind.Simp
 import Lean.Meta.Tactic.Grind.Ctor
+import Lean.Meta.Tactic.Grind.Parser
 
 namespace Lean
 

src/Lean/Meta/Tactic/Grind/Parser.lean

@@ -0,0 +1,15 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Parser.Command
+
+namespace Lean.Parser.Command
+/-!
+Builtin parsers for `grind` related commands
+-/
+@[builtin_command_parser] def grindPattern := leading_parser
+  "grind_pattern " >>  ident >> darrow >> sepBy1 termParser ","
+end Lean.Parser.Command