From e3ccc03a45992ef35e2f6947d7a3458c230bfd5b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 1 Sep 2021 18:44:35 -0700
Subject: [PATCH] chore: add nested conv tactics

---
 src/Init/Conv.lean                   | 5 +++++
 src/Lean/Elab/Tactic/Conv/Basic.lean | 6 ++++++
 tests/lean/run/conv1.lean            | 5 ++---
 3 files changed, 13 insertions(+), 3 deletions(-)

diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean
index 86afc97ab0..819224cd8e 100644
--- a/src/Init/Conv.lean
+++ b/src/Init/Conv.lean
@@ -21,6 +21,11 @@ syntax (name := lhs) "lhs" : conv
 syntax (name := rhs) "rhs" : conv
 syntax (name := whnf) "whnf" : conv
 syntax (name := congr) "congr" : conv
+syntax (name := nestedConv) convSeqBracketed : conv
+syntax (name := paren) "(" convSeq ")" : conv
+
+/-- `· conv` focuses on the main conv goal and tries to solve it using `s` -/
+macro dot:("·" <|> ".") s:convSeq : conv => `(conv| {%$dot ($s:convSeq) })
 
 syntax (name := conv) "conv " (" at " ident)? (" in " term)? " => " convSeq : tactic
 
diff --git a/src/Lean/Elab/Tactic/Conv/Basic.lean b/src/Lean/Elab/Tactic/Conv/Basic.lean
index 72b5534f26..97007c5125 100644
--- a/src/Lean/Elab/Tactic/Conv/Basic.lean
+++ b/src/Lean/Elab/Tactic/Conv/Basic.lean
@@ -75,9 +75,15 @@ def changeLhs (lhs' : Expr) : TacticM Unit := do
 @[builtinTactic Lean.Parser.Tactic.Conv.convSeqBracketed] def evalConvSeqBracketed : Tactic := fun stx => do
   evalTacticSeqBracketed stx
 
+@[builtinTactic Lean.Parser.Tactic.Conv.nestedConv] def evalNestedConv : Tactic := fun stx => do
+  evalTacticSeqBracketed stx[0]
+
 @[builtinTactic Lean.Parser.Tactic.Conv.convSeq] def evalConvSeq : Tactic := fun stx => do
   evalTactic stx[0]
 
+@[builtinTactic Lean.Parser.Tactic.Conv.paren] def evalParen : Tactic := fun stx =>
+  evalTactic stx[1]
+
 private def convTarget (conv : Syntax) : TacticM Unit := do
    let target ← getMainTarget
    let (targetNew, proof) ← convert target (evalTactic conv)
diff --git a/tests/lean/run/conv1.lean b/tests/lean/run/conv1.lean
index 6adeadd120..78ab3cf918 100644
--- a/tests/lean/run/conv1.lean
+++ b/tests/lean/run/conv1.lean
@@ -6,9 +6,8 @@ example (x y : Nat) : p (x + y) (y + x + 0) := by
   conv =>
     whnf
     congr
-    skip
-    whnf
-    skip
+    . skip
+    . whnf; skip
   traceState
   rw [Nat.add_comm]
   rfl