From 2ead798d877e49794b4dca7bd88d301b24338523 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 20 Oct 2025 17:53:35 -0700 Subject: [PATCH] fix: `set_option` auto-completion in `grind` mode (#10859) This PR fixes auto-completion for `set_option` in `grind` interactive mode. --- src/Init/Grind/Interactive.lean | 2 +- src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Init/Grind/Interactive.lean b/src/Init/Grind/Interactive.lean index f3004385e8..7df86d5fce 100644 --- a/src/Init/Grind/Interactive.lean +++ b/src/Init/Grind/Interactive.lean @@ -192,7 +192,7 @@ syntax (name := exposeNames) "expose_names" : grind /-- `set_option opt val in tacs` (the tactic) acts like `set_option opt val` at the command level, but it sets the option only within the tactics `tacs`. -/ -syntax (name := setOption) "set_option " ident ppSpace optionValue " in " grindSeq : grind +syntax (name := setOption) "set_option " (ident (noWs "." noWs ident)?) ppSpace optionValue " in " grindSeq : grind end Grind end Lean.Parser.Tactic diff --git a/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean b/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean index d6f95f3665..36f3d11162 100644 --- a/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean +++ b/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean @@ -426,7 +426,7 @@ where replaceMainGoal [{ goal with mvarId }] @[builtin_grind_tactic setOption] def elabSetOption : GrindTactic := fun stx => do - let options ← Elab.elabSetOption stx[1] stx[2] - withOptions (fun _ => options) do evalGrindTactic stx[4] + let options ← Elab.elabSetOption stx[1] stx[3] + withOptions (fun _ => options) do evalGrindTactic stx[5] end Lean.Elab.Tactic.Grind