diff --git a/src/Lean/Meta/Tactic/Grind.lean b/src/Lean/Meta/Tactic/Grind.lean index eea764d89e39..3b9b4e094412 100644 --- a/src/Lean/Meta/Tactic/Grind.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Grind/Parser.lean b/src/Lean/Meta/Tactic/Grind/Parser.lean new file mode 100644 index 000000000000..9efae2a380ac --- /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