chore: init_grind_norm command parser

2026-03-21 04:14:07 +00:00 · 2025-01-18 14:46:52 -08:00
1 changed files with 4 additions and 0 deletions
--- a/src/Lean/Meta/Tactic/Grind/Parser.lean
+++ b/src/Lean/Meta/Tactic/Grind/Parser.lean
@@ -12,4 +12,8 @@ Builtin parsers for `grind` related commands
 -/
@[builtin_command_parser] def grindPattern := leading_parser
  "grind_pattern " >>  ident >> darrow >> sepBy1 termParser ","
+
+@[builtin_command_parser] def initGrindNorm := leading_parser
+  "init_grind_norm " >> many ident >> "| " >> many ident
+
 end Lean.Parser.Command