From 45744cc8b12e6cf5b3725720a9dfe5edc291ba24 Mon Sep 17 00:00:00 2001
From: lecopivo <skrivantomas@seznam.cz>
Date: Wed, 15 Nov 2023 14:45:04 -0500
Subject: [PATCH 1/2] feat: set_option inside conv mode

---
 src/Lean/Elab/Tactic/Conv/Basic.lean       | 14 ++++++++++++++
 tests/lean/setOptionConv.lean              | 21 +++++++++++++++++++++
 tests/lean/setOptionConv.lean.expected.out |  8 ++++++++
 3 files changed, 43 insertions(+)
 create mode 100644 tests/lean/setOptionConv.lean
 create mode 100644 tests/lean/setOptionConv.lean.expected.out

diff --git a/src/Lean/Elab/Tactic/Conv/Basic.lean b/src/Lean/Elab/Tactic/Conv/Basic.lean
index bc4bb3ce7632..306bd55833a3 100644
--- a/src/Lean/Elab/Tactic/Conv/Basic.lean
+++ b/src/Lean/Elab/Tactic/Conv/Basic.lean
@@ -187,3 +187,17 @@ private def convLocalDecl (conv : Syntax) (hUserName : Name) : TacticM Unit := w
   Tactic.evalFirst
 
 end Lean.Elab.Tactic.Conv
+
+open Lean.Parser Tactic.Conv in
+/-- `set_option opt val in tacs` (the conv tactic) acts like `set_option opt val` at the command level,
+but it sets the option only within the conv tactics `tacs`. -/
+syntax (name := Lean.Parser.Tactic.Conv.«set_option») "set_option " ident ppSpace Lean.Parser.Command.optionValue " in " convSeq : conv
+
+namespace Lean.Elab.Tactic.Conv
+
+@[builtin_tactic Lean.Parser.Tactic.Conv.set_option] def elabSetOption : Tactic := fun stx => do
+  let options ← Elab.elabSetOption stx[1] stx[2]
+  withTheReader Core.Context (fun ctx => { ctx with maxRecDepth := maxRecDepth.get options, options := options }) do
+    evalTactic stx[4]
+
+end Lean.Elab.Tactic.Conv
diff --git a/tests/lean/setOptionConv.lean b/tests/lean/setOptionConv.lean
new file mode 100644
index 000000000000..ef1c27933b5c
--- /dev/null
+++ b/tests/lean/setOptionConv.lean
@@ -0,0 +1,21 @@
+import Lean
+
+example 
+  : (fun x : Nat => x + 0)
+    =
+    fun x => x
+  := 
+by
+  trace_state
+  set_option pp.funBinderTypes true in
+  trace_state; trace_state
+  trace_state
+
+  set_option pp.funBinderTypes false in
+
+  conv => 
+    trace_state
+    set_option pp.funBinderTypes true in
+    trace_state; trace_state
+    trace_state
+
diff --git a/tests/lean/setOptionConv.lean.expected.out b/tests/lean/setOptionConv.lean.expected.out
new file mode 100644
index 000000000000..bcfc3df8e370
--- /dev/null
+++ b/tests/lean/setOptionConv.lean.expected.out
@@ -0,0 +1,8 @@
+⊢ (fun x => x + 0) = fun x => x
+⊢ (fun (x : Nat) => x + 0) = fun (x : Nat) => x
+⊢ (fun (x : Nat) => x + 0) = fun (x : Nat) => x
+⊢ (fun (x : Nat) => x + 0) = fun (x : Nat) => x
+| (fun x => x + 0) = fun x => x
+| (fun (x : Nat) => x + 0) = fun (x : Nat) => x
+| (fun (x : Nat) => x + 0) = fun (x : Nat) => x
+| (fun (x : Nat) => x + 0) = fun (x : Nat) => x

From d00796640c138b720ffe2f58e5b60318dd65d177 Mon Sep 17 00:00:00 2001
From: lecopivo <skrivantomas@seznam.cz>
Date: Wed, 15 Nov 2023 14:50:57 -0500
Subject: [PATCH 2/2] chore: proper place for Conv.set_option parser

---
 src/Lean/Parser/Command.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index 5bad70f87e18..6d65d6cbfc0a 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -343,6 +343,11 @@ but it opens a namespace only within the tactics `tacs`. -/
 but it sets the option only within the tactics `tacs`. -/
 @[builtin_tactic_parser] def «set_option» := leading_parser:leadPrec
   "set_option " >> ident >> ppSpace >> Command.optionValue >> " in " >> tacticSeq
+
+-- /-- `set_option opt val in tacs` (the conv tactic) acts like `set_option opt val` at the command level,
+-- but it sets the option only within the conv tactics `tacs`. -/
+-- @[builtin_tactic_parser] def Conv.«set_option» := leading_parser:leadPrec
+--   "set_option " >> ident >> ppSpace >> Command.optionValue >> " in " >> convSeq
 end Tactic
 
 end Parser