diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean
index 1a15193cc0..75f6ebcbb8 100644
--- a/src/Init/Conv.lean
+++ b/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
diff --git a/src/Lean/Elab/Tactic/Conv/Basic.lean b/src/Lean/Elab/Tactic/Conv/Basic.lean
index 1c6e5873ed..ea17fa9ecb 100644
--- a/src/Lean/Elab/Tactic/Conv/Basic.lean
+++ b/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
diff --git a/tests/lean/run/repeatConv.lean b/tests/lean/run/repeatConv.lean
new file mode 100644
index 0000000000..f731817ab2
--- /dev/null
+++ b/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]