From 85f2213d5a9a5e8cf09a5a61501576848ae8d144 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Fri, 8 Nov 2024 04:36:49 -0800 Subject: [PATCH] fix: unset trailing for `simpa?` "try this" suggestion (#5907) Closes #4581 --- src/Lean/Elab/Tactic/Simpa.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Lean/Elab/Tactic/Simpa.lean b/src/Lean/Elab/Tactic/Simpa.lean index a3a70f49fd9f..40e38289610e 100644 --- a/src/Lean/Elab/Tactic/Simpa.lean +++ b/src/Lean/Elab/Tactic/Simpa.lean @@ -95,7 +95,8 @@ deriving instance Repr for UseImplicitLambdaResult else g.assumption; pure stats if tactic.simp.trace.get (← getOptions) || squeeze.isSome then - let stx ← match ← mkSimpOnly stx stats.usedTheorems with + let usingArg : Option Term := usingArg.map (⟨·.raw.unsetTrailing⟩) + let stx ← match ← mkSimpOnly stx.raw.unsetTrailing stats.usedTheorems with | `(tactic| simp $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]?) => if unfold.isSome then `(tactic| simpa! $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?)