refactor: use partial_fixpoint/MonadTail for Repeat loops

Replace the `extrinsicFix`/`MonadAttach` approach with Lean's existing
`partial_fixpoint` mechanism and a new `MonadTail` class (weaker than
`MonoBind`, requiring only bind monotonicity in the continuation).

Key changes:
- Rename `MonoBindRight` to `MonadTail` with scoped monotonicity attribute
- Rewrite `Repeat.forIn` using `partial_fixpoint` recursion
- Move `RepeatVariant`/`RepeatInvariant` to `RepeatSpec.lean`
- Add `MonadTail` instances for `BaseAsync`, `EAsync`, `ContextAsync`
- Add axiom `BaseAsync.bind_mono_right'` for opaque `BaseIO.bindTask`
- Simplify `elabDoRepeat` (remove try/catch fallback)
- Remove `WPAdequacy`, `MonadAttach` instances, `RepeatCursor`

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

src/Init.lean

@@ -40,6 +40,7 @@ public import Init.Grind
 public import Init.GrindInstances
 public import Init.Sym
 public import Init.While
+public import Init.Repeat
 public import Init.Syntax
 public import Init.Internal
 public import Init.Try

src/Init/Internal/Order.lean

@@ -8,4 +8,5 @@ module
 prelude
 public import Init.Internal.Order.Basic
 public import Init.Internal.Order.Lemmas
+public import Init.Internal.Order.MonadTail
 public import Init.Internal.Order.Tactic

src/Init/Internal/Order/MonadTail.lean

@@ -0,0 +1,140 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+module
+
+prelude
+public import Init.Internal.Order.Basic
+import all Init.System.ST  -- for EST.bind in MonadTail instance
+
+set_option linter.missingDocs true
+
+public section
+
+namespace Lean.Order
+
+/--
+A *tail monad* is a monad whose bind operation preserves any suitable ordering of the continuation.
+Specifically, `MonadTail m` asserts that every `m β` carries a chain-complete partial order (CCPO)
+and that `>>=` is monotone in its second (continuation) argument with respect to that order.
+
+This is a weaker requirement than `MonoBind`, which requires monotonicity in both arguments.
+`MonadTail` is sufficient for `partial_fixpoint`-based recursive definitions where the
+recursive call only appears in the continuation (second argument) of `>>=`.
+-/
+class MonadTail (m : Type u → Type v) [Bind m] where
+  /-- Every `m β` with `Nonempty β` has a chain-complete partial order. -/
+  instCCPO β [Nonempty β] : CCPO (m β)
+  /-- Bind is monotone in the second (continuation) argument. -/
+  bind_mono_right {a : m α} {f₁ f₂ : α → m β} [Nonempty β] (h : ∀ x, f₁ x ⊑ f₂ x) :
+    a >>= f₁ ⊑ a >>= f₂
+
+attribute [implicit_reducible] MonadTail.instCCPO
+attribute [instance] MonadTail.instCCPO
+
+@[scoped partial_fixpoint_monotone]
+theorem MonadTail.monotone_bind_right
+    (m : Type u → Type v) [Monad m] [MonadTail m]
+    {α β : Type u} [Nonempty β]
+    {γ : Sort w} [PartialOrder γ]
+    (f : m α) (g : γ → α → m β)
+    (hmono : monotone g) :
+    monotone (fun (x : γ) => f >>= g x) :=
+  fun _ _ h => MonadTail.bind_mono_right (hmono _ _ h)
+
+instance : MonadTail Id where
+  instCCPO _ := inferInstanceAs (CCPO (FlatOrder (b := Classical.ofNonempty)))
+  bind_mono_right h := h _
+
+instance {σ : Type u} {m : Type u → Type v} [Monad m] [MonadTail m] [Nonempty σ] :
+    MonadTail (StateT σ m) where
+  instCCPO α := inferInstanceAs (CCPO (σ → m (α × σ)))
+  bind_mono_right h := by
+    intro s
+    show StateT.bind _ _ s ⊑ StateT.bind _ _ s
+    simp only [StateT.bind]
+    apply MonadTail.bind_mono_right (m := m)
+    intro ⟨x, s'⟩
+    exact h x s'
+
+instance {ε : Type u} {m : Type u → Type v} [Monad m] [MonadTail m] :
+    MonadTail (ExceptT ε m) where
+  instCCPO β := MonadTail.instCCPO (Except ε β)
+  bind_mono_right h := by
+    apply MonadTail.bind_mono_right (m := m)
+    intro x
+    cases x with
+    | error => exact PartialOrder.rel_refl
+    | ok a => exact h a
+
+instance : MonadTail (Except ε) where
+  instCCPO β := inferInstanceAs (CCPO (FlatOrder (b := Classical.ofNonempty)))
+  bind_mono_right h := by
+    cases ‹Except _ _› with
+    | error => exact FlatOrder.rel.refl
+    | ok a => exact h a
+
+instance {m : Type u → Type v} [Monad m] [MonadTail m] :
+    MonadTail (OptionT m) where
+  instCCPO β := MonadTail.instCCPO (Option β)
+  bind_mono_right h := by
+    apply MonadTail.bind_mono_right (m := m)
+    intro x
+    cases x with
+    | none => exact PartialOrder.rel_refl
+    | some a => exact h a
+
+instance : MonadTail Option where
+  instCCPO _ := inferInstance
+  bind_mono_right h := MonoBind.bind_mono_right h
+
+instance {ρ : Type u} {m : Type u → Type v} [Monad m] [MonadTail m] :
+    MonadTail (ReaderT ρ m) where
+  instCCPO α := inferInstanceAs (CCPO (ρ → m α))
+  bind_mono_right h := by
+    intro r
+    show ReaderT.bind _ _ r ⊑ ReaderT.bind _ _ r
+    simp only [ReaderT.bind]
+    apply MonadTail.bind_mono_right (m := m)
+    intro x
+    exact h x r
+
+set_option linter.missingDocs false in
+noncomputable def ST.bot' [Nonempty α] (s : Void σ) : @FlatOrder (ST.Out σ α) (.mk Classical.ofNonempty (Classical.choice ⟨s⟩)) :=
+  .mk Classical.ofNonempty (Classical.choice ⟨s⟩)
+
+instance [Nonempty α] : CCPO (ST σ α) where
+  rel := PartialOrder.rel (α := ∀ s, FlatOrder (ST.bot' s))
+  rel_refl := PartialOrder.rel_refl
+  rel_antisymm := PartialOrder.rel_antisymm
+  rel_trans := PartialOrder.rel_trans
+  has_csup hchain := CCPO.has_csup (α := ∀ s, FlatOrder (ST.bot' s)) hchain
+
+instance : MonadTail (ST σ) where
+  instCCPO _ := inferInstance
+  bind_mono_right {_ _ a f₁ f₂} _ h := by
+    intro w
+    change FlatOrder.rel (ST.bind a f₁ w) (ST.bind a f₂ w)
+    simp only [ST.bind]
+    apply h
+
+instance : MonadTail BaseIO :=
+  inferInstanceAs (MonadTail (ST IO.RealWorld))
+
+instance [Nonempty ε] : MonadTail (EST ε σ) where
+  instCCPO _ := inferInstance
+  bind_mono_right h := MonoBind.bind_mono_right h
+
+instance [Nonempty ε] : MonadTail (EIO ε) :=
+  inferInstanceAs (MonadTail (EST ε IO.RealWorld))
+
+instance : MonadTail IO :=
+  inferInstanceAs (MonadTail (EIO IO.Error))
+
+instance {ω : Type} {σ : Type} {m : Type → Type} [Monad m] [MonadTail m] :
+    MonadTail (StateRefT' ω σ m) :=
+  inferInstanceAs (MonadTail (ReaderT (ST.Ref ω σ) m))
+
+end Lean.Order

src/Init/Repeat.lean

@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+module
+
+prelude
+public import Init.Core
+public import Init.Internal.Order.MonadTail
+import Init.While
+
+set_option linter.missingDocs true
+
+@[expose] public section
+
+namespace Lean
+
+open Lean.Order
+
+/-!
+# `Repeat` type for verified `repeat`/`while` loops
+
+This module provides a `Repeat` type that serves as an alternative to `Loop` for `repeat`/`while`
+loops. Unlike `Loop`, which uses `partial` recursion, `Repeat` is implemented using
+`partial_fixpoint` and `MonadTail`, enabling verified reasoning about loop programs.
+-/
+
+/-- A type for `repeat`/`while` loops that supports verified reasoning via `partial_fixpoint`. -/
+structure Repeat where
+
+set_option linter.missingDocs false in
+open Lean.Order.MonadTail in
+def Repeat.forIn {β : Type u} {m : Type u → Type v}
+    [Nonempty β] [Monad m] [Lean.Order.MonadTail m]
+    (b : β) (f : Unit → β → m (ForInStep β)) : m β := do
+  match ← f () b with
+  | ForInStep.done b => pure b
+  | ForInStep.yield b => Repeat.forIn b f
+partial_fixpoint
+
+instance [Monad m] [Lean.Order.MonadTail m] : ForIn m Repeat Unit where
+  forIn _ init f := haveI : Nonempty _ := ⟨init⟩; Repeat.forIn init f
+
+macro_rules
+  | `(doElem| repeat $seq) => do
+    if ← Macro.hasDecl `Lean.Elab.Do.elabDoRepeat then
+      Lean.Macro.throwUnsupported
+    `(doElem| for _ in Repeat.mk do $seq)
+
+end Lean

src/Init/While.lean

@@ -32,8 +32,11 @@ partial def Loop.forIn {β : Type u} {m : Type u → Type v} [Monad m] (_ : Loop
 instance [Monad m] : ForIn m Loop Unit where
   forIn := Loop.forIn
 
-syntax "repeat " doSeq : doElem
+syntax (name := doRepeat) "repeat " doSeq : doElem
 
+/-- Bootstrapping fallback macro for `repeat`.
+Expands to `for _ in Loop.mk do ...`. Overridden by the macro in `Init.Repeat` after
+bootstrapping. -/
 macro_rules
   | `(doElem| repeat $seq) => `(doElem| for _ in Loop.mk do $seq)
 

src/Lean/Elab/BuiltinDo.lean

@@ -15,3 +15,4 @@ public import Lean.Elab.BuiltinDo.Jump
 public import Lean.Elab.BuiltinDo.Misc
 public import Lean.Elab.BuiltinDo.For
 public import Lean.Elab.BuiltinDo.TryCatch
+public import Lean.Elab.BuiltinDo.Repeat

src/Lean/Elab/BuiltinDo/Repeat.lean

@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+module
+
+prelude
+public import Lean.Elab.BuiltinDo.Basic
+meta import Lean.Parser.Do
+import Lean.Elab.BuiltinDo.For
+import Lean.Elab.Do.Switch
+
+public section
+
+namespace Lean.Elab.Do
+
+open Lean.Parser.Term
+
+@[builtin_doElem_elab Lean.doRepeat] def elabDoRepeat : DoElab := fun stx dec => do
+  let `(doElem| repeat $seq) := stx | throwUnsupportedSyntax
+  let expanded ←
+    if Term.backward.do.while.get (← getOptions) then
+      `(doElem| for _ in Loop.mk do $seq)
+    else
+      `(doElem| for _ in Repeat.mk do $seq)
+  Term.withMacroExpansion stx expanded <|
+    withRef expanded <| elabDoElem ⟨expanded⟩ dec
+
+end Lean.Elab.Do

src/Lean/Elab/Do/Legacy.lean

@@ -1780,6 +1780,10 @@ mutual
             doIfToCode doElem doElems
           else if k == ``Parser.Term.doUnless then
             doUnlessToCode doElem doElems
+          else if k == `Lean.doRepeat then
+            let seq := doElem[1]
+            let expanded ← `(doElem| for _ in Loop.mk do $seq)
+            doSeqToCode (expanded :: doElems)
           else if k == ``Parser.Term.doFor then withFreshMacroScope do
             doForToCode doElem doElems
           else if k == ``Parser.Term.doMatch then

src/Lean/Elab/Do/Switch.lean

@@ -19,6 +19,11 @@ register_builtin_option backward.do.legacy : Bool := {
   descr    := "Use the legacy `do` elaborator instead of the new, extensible implementation."
 }
 
+register_builtin_option backward.do.while : Bool := {
+  defValue := false
+  descr    := "Use the legacy partial `Loop` type for `repeat`/`while` loops instead of `Repeat`, which is based on `partial_fixpoint`. Useful as a workaround when the monad lacks a `MonadTail` instance."
+}
+
 private def toDoElem (newKind : SyntaxNodeKind) : Macro := fun stx => do
   let stx := stx.setKind newKind
   withRef stx `(do $(⟨stx⟩):doElem)

src/Std/Do/SPred/DerivedLaws.lean

@@ -178,6 +178,36 @@ theorem entails_pure_elim_cons {σ : Type u} [Inhabited σ] (P Q : Prop) : entai
 @[simp] theorem entails_4 {P Q : SPred [σ₁, σ₂, σ₃, σ₄]} : SPred.entails P Q ↔ (∀ s₁ s₂ s₃ s₄, (P s₁ s₂ s₃ s₄).down → (Q s₁ s₂ s₃ s₄).down) := iff_of_eq rfl
 @[simp] theorem entails_5 {P Q : SPred [σ₁, σ₂, σ₃, σ₄, σ₅]} : SPred.entails P Q ↔ (∀ s₁ s₂ s₃ s₄ s₅, (P s₁ s₂ s₃ s₄ s₅).down → (Q s₁ s₂ s₃ s₄ s₅).down) := iff_of_eq rfl
 
+/-!
+# `SPred.evalsTo`
+
+Relates a stateful value `SVal σs α` to a pure value `a : α`, lifting equality through the state.
+-/
+
+/-- Relates a stateful value to a pure value, lifting equality through the state layers. -/
+def evalsTo {α : Type u} {σs : List (Type u)} (f : SVal σs α) (a : α) : SPred σs :=
+  match σs with
+  | [] => ⌜a = f⌝
+  | _ :: _ => fun s => evalsTo (f s) a
+
+@[simp, grind =] theorem evalsTo_nil {f : SVal [] α} {a : α} :
+    evalsTo f a = ⌜a = f⌝ := rfl
+
+theorem evalsTo_cons {f : σ → SVal σs α} {a : α} {s : σ} :
+    evalsTo (σs := σ::σs) f a s = evalsTo (f s) a := rfl
+
+@[simp, grind =] theorem evalsTo_1 {f : SVal [σ] α} {a : α} {s : σ} :
+    evalsTo f a s = evalsTo (f s) a := rfl
+
+@[simp, grind =] theorem evalsTo_2 {f : SVal [σ₁, σ₂] α} {a : α} {s₁ : σ₁} {s₂ : σ₂} :
+    evalsTo f a s₁ s₂ = evalsTo (f s₁ s₂) a := rfl
+
+theorem evalsTo_total {P : SPred σs} (f : SVal σs α) :
+    P ⊢ₛ ∃ m, evalsTo f m := by
+  induction σs with
+  | nil => simp
+  | cons _ _ ih => intro s; apply ih
+
 /-! # Tactic support -/
 
 namespace Tactic
@@ -338,3 +368,4 @@ theorem Frame.frame {P Q T : SPred σs} {φ : Prop} [HasFrame P Q φ]
     · exact HasFrame.reassoc.mp.trans SPred.and_elim_r
     · intro hp
       exact HasFrame.reassoc.mp.trans (SPred.and_elim_l' (h hp))
+

src/Std/Do/SPred/Laws.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Std.Do.SPred.Notation
+import Init.PropLemmas
 
 @[expose] public section
 
@@ -157,3 +158,17 @@ theorem imp_curry {P Q : SVal.StateTuple σs → Prop} : (SVal.curry (fun t =>
   induction σs
   case nil => rfl
   case cons σ σs ih => intro s; simp only [imp_cons, SVal.curry_cons]; exact ih
+
+/-! # Prop-indexed quantifiers -/
+
+/-- Simplifies an existential over a true proposition. -/
+theorem exists_prop_of_true {p : Prop} (h : p) {P : p → SPred σs} : spred(∃ (h : p), P h) = P h := by
+  induction σs with
+  | nil => ext; exact _root_.exists_prop_of_true h
+  | cons σ σs ih => ext; exact ih
+
+/-- Simplifies a universal over a true proposition. -/
+theorem forall_prop_of_true {p : Prop} (h : p) {P : p → SPred σs} : spred(∀ (h : p), P h) = P h := by
+  induction σs with
+  | nil => ext; exact _root_.forall_prop_of_true h
+  | cons σ σs ih => ext; exact ih

src/Std/Do/Triple/RepeatSpec.lean

@@ -0,0 +1,94 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+module
+
+prelude
+public import Std.Do.Triple.SpecLemmas
+import Std.Tactic.Do.Syntax
+
+set_option linter.missingDocs true
+
+@[expose] public section
+
+namespace Std.Do
+
+/-!
+# Specification theorem for `Repeat` loops
+
+This file contains the `@[spec]` theorem for `forIn` over `Lean.Repeat`, which enables
+verified reasoning about `repeat`/`while` loops using `mvcgen`.
+-/
+
+set_option mvcgen.warning false
+
+/-- A variant (termination measure) for a `Repeat`/`while` loop. -/
+@[spec_invariant_type]
+abbrev RepeatVariant (β : Type u) (ps : PostShape.{u}) := β → SVal ps.args (ULift Nat)
+
+set_option linter.missingDocs false in
+abbrev RepeatVariant.eval {β ps} (variant : RepeatVariant β ps) (b : β) (n : Nat) :=
+  SPred.evalsTo (variant b) ⟨n⟩
+
+/-- An invariant for a `Repeat`/`while` loop. -/
+@[spec_invariant_type]
+abbrev RepeatInvariant β ps := PostCond (Bool × β) ps
+
+section
+
+variable {β : Type u} {m : Type u → Type v} {ps : PostShape.{u}}
+
+private theorem RepeatVariant.eval_total {P : SPred ps.args} (variant : RepeatVariant β ps) (b : β) :
+    P ⊢ₛ ∃ m, RepeatVariant.eval variant b m := by
+  mintro _
+  mhave h2 := SPred.evalsTo_total (variant b)
+  mcases h2 with ⟨m, h2⟩
+  mexists m.down
+
+private theorem RepeatVariant.add_eval {P Q : SPred ps.args} (variant : RepeatVariant β ps) (b : β)
+    (h : spred(∃ m, RepeatVariant.eval variant b m ∧ P) ⊢ₛ Q) : P ⊢ₛ Q := by
+  apply SPred.entails.trans _ h
+  mintro _
+  mhave h2 := RepeatVariant.eval_total variant b
+  mcases h2 with ⟨m, h2⟩
+  mexists m
+  mconstructor <;> massumption
+
+end
+
+section
+
+variable {β : Type u} {m : Type u → Type v} {ps : PostShape.{u}}
+variable [Monad m] [Lean.Order.MonadTail m] [WPMonad m ps]
+
+@[spec]
+theorem Spec.forIn_repeat
+    {l : _root_.Lean.Repeat} {init : β} {f : Unit → β → m (ForInStep β)}
+    (measure : RepeatVariant β ps)
+    (inv : RepeatInvariant β ps)
+    (step : ∀ b mb,
+      Triple (f () b)
+        spred(RepeatVariant.eval measure b mb ∧ inv.1 (false, b))
+        (fun r => match r with
+          | .yield b' => spred(∃ mb', RepeatVariant.eval measure b' mb' ∧ ⌜mb' < mb⌝ ∧ inv.1 (false, b'))
+          | .done b' => inv.1 (true, b'), inv.2)) :
+    Triple (forIn l init f) spred(inv.1 (false, init)) (fun b => inv.1 (true, b), inv.2) := by
+  haveI : Nonempty β := ⟨init⟩
+  simp only [forIn]
+  apply RepeatVariant.add_eval measure init
+  apply SPred.exists_elim
+  intro minit
+  induction minit using Nat.strongRecOn generalizing init with
+  | _ minit ih =>
+  rw [_root_.Lean.Repeat.forIn.eq_1]
+  mvcgen [step, ih] with
+  | vc2 =>
+    mrename_i h
+    mcases h with ⟨mb', ⟨hmeasure, ⌜hmb'⌝, h⟩⟩
+    mspec Triple.of_entails_wp (ih mb' hmb')
+
+end
+
+end Std.Do

src/Std/Do/Triple/SpecLemmas.lean

@@ -10,6 +10,7 @@ public import Std.Do.Triple.Basic
 public import Init.Data.Range.Polymorphic.Iterators
 import Init.Data.Range.Polymorphic
 public import Init.Data.Slice.Array
+public import Init.Repeat
 
 -- This public import is a workaround for #10652.
 -- Without it, adding the `spec` attribute for `instMonadLiftTOfMonadLift` will fail.
@@ -2188,3 +2189,5 @@ theorem Spec.forIn_stringSlice
       next => apply Triple.pure; simp
       next b => simp [ih _ _ hsp.next]
   | endPos => simpa using Triple.pure _ (by simp)
+
+

src/Std/Internal/Async/Basic.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Init.System.Promise
 public import Init.While
+public import Init.Internal.Order.MonadTail
 
 public section
 
@@ -487,6 +488,24 @@ instance : Monad BaseAsync where
   pure := BaseAsync.pure
   bind := BaseAsync.bind
 
+set_option linter.unusedVariables false in
+/-- `BaseAsync.bind` is monotone in the continuation argument with respect to the CCPO on
+`BaseAsync`. This is an axiom because the `MaybeTask.ofTask` case of `BaseAsync.bind` uses
+`BaseIO.bindTask`, which is `@[extern] opaque` and cannot be unfolded. The property holds
+because `bind` only calls the continuation on values produced by `a`. -/
+axiom bind_mono_right' {α β : Type} [inst : Nonempty (MaybeTask β)]
+    (a : BaseIO (MaybeTask α)) (f₁ f₂ : α → BaseIO (MaybeTask β))
+    (h : ∀ x, @Lean.Order.PartialOrder.rel (BaseIO (MaybeTask β)) (Lean.Order.CCPO.toPartialOrder) (f₁ x) (f₂ x)) :
+    @Lean.Order.PartialOrder.rel (BaseIO (MaybeTask β)) (Lean.Order.CCPO.toPartialOrder)
+      (BaseAsync.bind a f₁) (BaseAsync.bind a f₂)
+
+set_option linter.unusedVariables false in
+instance : Lean.Order.MonadTail BaseAsync where
+  instCCPO _ := inferInstanceAs (Lean.Order.CCPO (BaseIO _))
+  bind_mono_right {α β a f₁ f₂} _ h :=
+    haveI : Nonempty (MaybeTask β) := ⟨.pure Classical.ofNonempty⟩
+    bind_mono_right' (β := β) a f₁ f₂ h
+
 instance : MonadLift BaseIO BaseAsync where
   monadLift := BaseAsync.lift
 
@@ -707,6 +726,15 @@ instance : Monad (EAsync ε) where
   pure := EAsync.pure
   bind := EAsync.bind
 
+instance : Lean.Order.MonadTail (EAsync ε) where
+  instCCPO _ := inferInstanceAs (Lean.Order.CCPO (BaseAsync _))
+  bind_mono_right {α β a f₁ f₂} _ h := by
+    haveI : Nonempty (MaybeTask (Except ε β)) := ⟨.pure Classical.ofNonempty⟩
+    exact BaseAsync.bind_mono_right' a _ _ fun x =>
+      match x with
+      | Except.error _ => Lean.Order.PartialOrder.rel_refl
+      | Except.ok a => h a
+
 instance : MonadLift (EIO ε) (EAsync ε) where
   monadLift := EAsync.lift
 

src/Std/Internal/Async/ContextAsync.lean

@@ -256,6 +256,14 @@ instance [Inhabited α] : Inhabited (ContextAsync α) where
 instance : MonadAwait AsyncTask ContextAsync where
   await t := fun _ => await t
 
+instance : Lean.Order.MonadTail ContextAsync where
+  instCCPO α := inferInstanceAs (Lean.Order.CCPO (CancellationContext → Async α))
+  bind_mono_right h := by
+    intro ctx
+    apply Lean.Order.MonadTail.bind_mono_right (m := Async)
+    intro x
+    exact h x ctx
+
 end ContextAsync
 
 /--

src/Std/Tactic/Do.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Std.Tactic.Do.ProofMode
 public import Std.Tactic.Do.Syntax
+public import Std.Do.Triple.RepeatSpec
 
 @[expose] public section
 

tests/elab/repeat_extrinsic.lean

@@ -0,0 +1,142 @@
+module
+
+import Std
+
+set_option mvcgen.warning false
+
+open Std.Do
+
+/-!
+# Tests for `Repeat`/`while` loops with `partial_fixpoint`
+
+These tests verify that the `Repeat` type and its verification infrastructure work correctly
+using the `partial_fixpoint`-based approach with `MonadTail`.
+-/
+
+/-- `sqrt n` computes the integer square root of `n` using a `while` loop. -/
+def sqrt (n : Nat) : Id Nat := do
+  if n = 0 then
+    return 0
+  let mut i := 0
+  while i * i ≤ n
+  do
+    i := i + 1
+  return i - 1
+
+/-- The `sqrt` function returns the correct integer square root. -/
+theorem sqrt_correct :
+    ⦃⌜True⌝⦄ sqrt n ⦃⇓ res => ⌜res * res ≤ n ∧ n < (res + 1) * (res+1)⌝⦄ := by
+  mvcgen [sqrt]
+  invariants
+  | inv1 => fun i => ULift.up ((n + 2) - i)
+  | inv2 => ⇓ (done, i) => ⌜∀ j, j < i → j * j ≤ n⌝ ∧ ⌜done = true → n < i * i⌝
+  with (try grind)
+  | vc2 r _ hsqr _ _ =>
+    have : r ≤ n := Nat.le_trans (Nat.le_mul_self r) hsqr
+    grind
+  | vc5 res h =>
+    have : res - 1 < res := by grind
+    grind
+
+-- Verify sqrt computes correctly
+#guard Id.run (sqrt 0) == 0
+#guard Id.run (sqrt 1) == 1
+#guard Id.run (sqrt 4) == 2
+#guard Id.run (sqrt 8) == 2
+#guard Id.run (sqrt 9) == 3
+#guard Id.run (sqrt 15) == 3
+#guard Id.run (sqrt 16) == 4
+#guard Id.run (sqrt 100) == 10
+
+/-- `sqrtState n` is the same as `sqrt` but uses `StateT`. -/
+def sqrtState (n : Nat) : StateT Nat Id Nat := do
+  if n = 0 then
+    return 0
+  let mut i := 0
+  while i * i ≤ n
+  do
+    i := i + 1
+  return i - 1
+
+/-- The `sqrtState` function returns the correct integer square root. -/
+theorem sqrtState_correct :
+    ⦃⌜True⌝⦄ sqrtState n ⦃⇓ res => ⌜res * res ≤ n ∧ n < (res + 1) * (res+1)⌝⦄ := by
+  mvcgen [sqrtState]
+  invariants
+  | inv1 => fun i _ => ULift.up ((n + 2) - i)
+  | inv2 => ⇓ (done, i) => ⌜∀ j, j < i → j * j ≤ n⌝ ∧ ⌜done = true → n < i * i⌝
+  with (try grind)
+  | vc2 r _ hsqr _ _ _ =>
+    have : r ≤ n := Nat.le_trans (Nat.le_mul_self r) hsqr
+    grind
+  | vc5 res h _ =>
+    have : res - 1 < res := by grind
+    grind
+
+/-- A loop that only terminates when the initial value satisfies `i ≤ x`. -/
+def loopWithTerminationPrecond (x : Nat) : Id Nat := do
+  let mut i := 0
+  while i ≠ x do
+    i := i + 1
+  return i
+
+example : ⦃⌜True⌝⦄ loopWithTerminationPrecond x ⦃⇓ r => ⌜r = x⌝⦄ := by
+  mvcgen [loopWithTerminationPrecond] invariants
+  | inv1 => fun i => ULift.up (x - i)
+  | inv2 => ⇓ (done, i) => ⌜i ≤ x⌝ ∧ ⌜done = true → i = x⌝
+  with grind
+
+/-- A loop that only terminates when the initial *state* satisfies some invariant. -/
+def loopWithStatefulTerminationPrecond (x : Nat) : StateM Nat Nat := do
+  set 0
+  while (← get) ≠ x do
+    modify fun i => i + 1
+  get
+
+example : ⦃⌜True⌝⦄ loopWithStatefulTerminationPrecond x ⦃⇓ r => ⌜r = x⌝⦄ := by
+  mvcgen [loopWithStatefulTerminationPrecond] invariants
+  | inv1 => fun _ s => ULift.up (x - s)
+  | inv2 => ⇓ (done, _) s => ⌜s ≤ x ∧ (done = true → s = x)⌝
+  with (try grind)
+
+/-- A loop that does not terminate for all inputs. -/
+def possiblyDivergentLoop (x : Nat) : Id Nat := do
+  let mut x := x
+  while x ≠ 20 do
+    x := x + 1
+  return x
+
+example : ⦃⌜x ≤ 20⌝⦄ possiblyDivergentLoop x ⦃⇓ r => ⌜r = 20⌝⦄ := by
+  mvcgen [possiblyDivergentLoop] invariants
+  | inv1 => fun i => ULift.up (20 - i)
+  | inv2 => ⇓ (done, i) => ⌜i ≤ 20⌝ ∧ ⌜done = true → i = 20⌝
+  with grind
+
+set_option backward.do.while true in
+/-- Test: `backward.do.while true` should expand to `Loop.mk`. -/
+def loopBackwardCompat (n : Nat) : Nat := Id.run do
+  let mut i := 0
+  repeat
+    if i < n then
+      i := i + 1
+    else
+      break
+  return i
+
+-- Verify the backward-compat loop computes correctly
+#guard loopBackwardCompat 5 == 5
+#guard loopBackwardCompat 0 == 0
+
+/-- Test: default setting should expand to `Repeat.mk`. -/
+def loopDefault (n : Nat) : Nat := Id.run do
+  let mut i := 0
+  repeat
+    if i < n then
+      i := i + 1
+    else
+      break
+  return i
+
+-- Verify the default loop computes correctly
+#guard loopDefault 5 == 5
+#guard loopDefault 0 == 0