max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: set_option auto-completion in grind mode (#10859)

Browse source 
This PR fixes auto-completion for `set_option` in `grind` interactive
mode.
This commit is contained in:
Leonardo de Moura 2025-10-20 17:53:35 -07:00 • committed by GitHub
parent baacf86e7f
commit 2ead798d87
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Grind/Interactive.lean
View file

@ -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

4
src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean
View file

@ -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