feat: add repeat tactic to conv mode

src/Init/Conv.lean

@@ -62,4 +62,11 @@ macro "done" : conv => `(tactic' => done)
 macro "trace_state" : conv => `(tactic' => trace_state)
 macro "apply " e:term : conv => `(tactic => apply $e)
 
+/-- `first | conv | ...` runs each `conv` until one succeeds, or else fails. -/
+syntax (name := first) "first " withPosition((group(colGe "|" convSeq))+) : conv
+
+syntax "repeat " convSeq : conv
+macro_rules
+  | `(conv| repeat $seq) => `(conv| first | ($seq); repeat $seq | skip)
+
 end Lean.Parser.Tactic.Conv

src/Lean/Elab/Tactic/Conv/Basic.lean

@@ -147,4 +147,7 @@ private def convLocalDecl (conv : Syntax) (hUserName : Name) : TacticM Unit := w
       convTarget code
   | _ => throwUnsupportedSyntax
 
+@[builtinTactic Lean.Parser.Tactic.Conv.first] partial def evalFirst : Tactic :=
+  Tactic.evalFirst
+
 end Lean.Elab.Tactic.Conv

tests/lean/run/repeatConv.lean

@@ -0,0 +1,5 @@
+example : (fun x y => (0 + x) + (0 + y)) = Nat.add := by
+  conv =>
+    lhs
+    intro x y
+    repeat rw [Nat.zero_add]