chore: add nested conv tactics

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
 

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)

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