feat: add `grind_pattern` command

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

diff --git a/src/Lean/Meta/Tactic/Grind.lean b/src/Lean/Meta/Tactic/Grind.lean
index eea764d..3b9b4e0 100644
--- a/src/Lean/Meta/Tactic/Grind.lean
+++ b/src/Lean/Meta/Tactic/Grind.lean
@@ -20,6 +20,7 @@
 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

diff --git a/src/Lean/Meta/Tactic/Grind/Parser.lean b/src/Lean/Meta/Tactic/Grind/Parser.lean
new file mode 100644
index 0000000..9efae2a
--- /dev/null
+++ b/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