diff --git a/src/Lean/Elab/BuiltinDo/Repeat.lean b/src/Lean/Elab/BuiltinDo/Repeat.lean
index e3714abaf5..1ab6907157 100644
--- a/src/Lean/Elab/BuiltinDo/Repeat.lean
+++ b/src/Lean/Elab/BuiltinDo/Repeat.lean
@@ -36,12 +36,8 @@ remove the following code without breaking the do block's type.
   Term.withMacroExpansion stx expanded <|
     withRef expanded <| elabDoElem ⟨expanded⟩ dec
 
-@[builtin_macro Lean.Parser.Term.doWhileH] def expandDoWhileH : Macro
-  | `(doElem| while%$tk $h : $cond do $seq) => `(doElem| repeat%$tk if $h:ident : $cond then $seq else break)
-  | _ => Macro.throwUnsupported
-
 @[builtin_macro Lean.Parser.Term.doWhile] def expandDoWhile : Macro
-  | `(doElem| while%$tk $cond do $seq) => `(doElem| repeat%$tk if $cond then $seq else break)
+  | `(doElem| while%$tk $cond:doIfCond do $seq) => `(doElem| repeat%$tk if $cond:doIfCond then $seq else break)
   | _ => Macro.throwUnsupported
 
 @[builtin_macro Lean.Parser.Term.doRepeatUntil] def expandDoRepeatUntil : Macro
diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean
index 3e785f4ae9..6a18fc424b 100644
--- a/src/Lean/Parser/Do.lean
+++ b/src/Lean/Parser/Do.lean
@@ -275,10 +275,8 @@ with debug assertions enabled (see the `debugAssertions` option).
 
 @[builtin_doElem_parser] def doRepeat      := leading_parser
   "repeat " >> doSeq
-@[builtin_doElem_parser] def doWhileH      := leading_parser
-  "while " >> ident >> " : " >> withForbidden "do" termParser >> " do " >> doSeq
 @[builtin_doElem_parser] def doWhile       := leading_parser
-  "while " >> withForbidden "do" termParser >> " do " >> doSeq
+  "while " >> withForbidden "do" doIfCond >> " do " >> doSeq
 @[builtin_doElem_parser] def doRepeatUntil := leading_parser
   "repeat " >> doSeq >> ppDedent ppLine >> "until " >> termParser
 
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index e444447049..a814500e6b 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -26,6 +26,7 @@ options get_default_options() {
     // Temporary, core-only flags for editing (i.e. must be part of stage0/bin/lean). Must be synced
     // with `LEAN_EXTRA_MAKE_OPTS` build flags in src/CMakeLists.txt.
     opts = opts.update({"backward", "do", "legacy"}, false);
+    // trigger stage0 update: unify `while` parser via `doIfCond`
 #endif
     return opts;
 }
diff --git a/tests/elab/whileRepeat.lean b/tests/elab/whileRepeat.lean
index bde2de6ada..91ab0c9d4b 100644
--- a/tests/elab/whileRepeat.lean
+++ b/tests/elab/whileRepeat.lean
@@ -48,3 +48,71 @@ test3 done 12
 -/
 #guard_msgs in
 #eval test3
+
+-- `while let pat := e do ...` exits when the pattern fails to match.
+def testWhileLet : IO Unit := do
+  let mut xs := [0, 1, 2, 3]
+  while let x :: rest := xs do
+    println! "{x}"
+    xs := rest
+  println! "done {xs.length}"
+
+/--
+info: 0
+1
+2
+3
+done 0
+-/
+#guard_msgs in
+#eval testWhileLet
+
+-- `while let pat ← e do ...` evaluates the bind on each iteration.
+def testWhileLetBind : IO Unit := do
+  let mut xs := [0, 1, 2, 3]
+  while let some x ← pure xs.head? do
+    println! "{x}"
+    xs := xs.tail
+  println! "done"
+
+/--
+info: 0
+1
+2
+3
+done
+-/
+#guard_msgs in
+#eval testWhileLetBind
+
+-- Pops entries from an `IO.Ref`-backed list to show that the bound expression
+-- in `while let pat ← e do ...` is re-evaluated each iteration.
+def testWhileLetBindRef : IO Unit := do
+  let r ← IO.mkRef [0, 1, 2, 3]
+  while let x :: rest ← r.get do
+    println! "{x}"
+    r.set rest
+  println! "done {(← r.get).length}"
+
+/--
+info: 0
+1
+2
+3
+done 0
+-/
+#guard_msgs in
+#eval testWhileLetBindRef
+
+-- Unified `while` keeps supporting the `while h : cond do ...` form.
+def testWhileH (xs : Array Nat) : Nat := Id.run do
+  let mut i := 0
+  let mut sum := 0
+  while h : i < xs.size do
+    sum := sum + xs[i]
+    i := i + 1
+  return sum
+
+/-- info: 6 -/
+#guard_msgs in
+#eval testWhileH #[1, 2, 3]