From fd41c691b2d0ed948feff777bf7bd6ca5b2be607 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 8 Jan 2025 14:21:32 +0100 Subject: [PATCH] chore: work around `grind` bootstrap issue --- src/Lean/Elab/Tactic/Grind.lean | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/src/Lean/Elab/Tactic/Grind.lean b/src/Lean/Elab/Tactic/Grind.lean index d094ae98e4bb..935b5e5ffd97 100644 --- a/src/Lean/Elab/Tactic/Grind.lean +++ b/src/Lean/Elab/Tactic/Grind.lean @@ -56,14 +56,14 @@ private def elabFallback (fallback? : Option Term) : TermElabM (Grind.GoalM Unit pure auxDeclName unsafe evalConst (Grind.GoalM Unit) auxDeclName -@[builtin_tactic Lean.Parser.Tactic.grind] def evalApplyRfl : Tactic := fun stx => do - match stx with - | `(tactic| grind $config:optConfig $[on_failure $fallback?]?) => - let fallback ← elabFallback fallback? - logWarningAt stx "The `grind` tactic is experimental and still under development. Avoid using it in production projects" - let declName := (← Term.getDeclName?).getD `_grind - let config ← elabGrindConfig config - withMainContext do liftMetaFinishingTactic (grind · config declName fallback) - | _ => throwUnsupportedSyntax +@[builtin_tactic Lean.Parser.Tactic.grind] def evalGrind : Tactic := fun stx => do + -- grind $config:optConfig $[on_failure $fallback?]? + let config := stx[1] + let fallback? := guard (stx[2].getNumArgs == 2) *> pure (TSyntax.mk stx[2][1]) + let fallback ← elabFallback fallback? + logWarningAt stx "The `grind` tactic is experimental and still under development. Avoid using it in production projects" + let declName := (← Term.getDeclName?).getD `_grind + let config ← elabGrindConfig config + withMainContext do liftMetaFinishingTactic (grind · config declName fallback) end Lean.Elab.Tactic