chore: revert "feat: add lake builtin-lint (#13422)

This PR reverts leanprover/lean4#13393.

src/Init/Internal/Order.lean

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

src/Init/Internal/Order/ExtrinsicFix.lean

@@ -1,117 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Graf, Robin Arnez
--/
-module
-
-prelude
-public import Init.Internal.Order.Basic
-public import Init.Internal.Order.MonadTail
-import Init.Classical
-
-set_option linter.missingDocs true
-
-/-!
-This module provides a fixpoint combinator that combines advantages of `partial` and
-`partial_fixpoint` recursion.
-
-The combinator is similar to {lean}`CCPO.fix`, but does not require a CCPO instance or
-monotonicity proof at the definition site. Therefore, it can be used in situations in which
-these constraints are unavailable (e.g., when the monad does not have a `MonadTail` instance).
-Given a CCPO and monotonicity proof, there are theorems guaranteeing that it equals
-{lean}`CCPO.fix` and satisfies fixpoint induction.
--/
-
-public section
-
-namespace Lean.Order
-
-/--
-The function implemented as the loop {lean}`opaqueFix f = f (opaqueFix f)`.
-{lean}`opaqueFix f` is the fixpoint of {name}`f`, as long as `f` is monotone with respect to
-some CCPO on `α`.
-
-The loop might run forever depending on {name}`f`. It is opaque, i.e., it is impossible to prove
-nontrivial properties about it.
--/
-@[specialize]
-partial def opaqueFix {α : Sort u} [Nonempty α] (f : α → α) : α :=
-  f (opaqueFix f)
-
-/-
-SAFE assuming that the code generated by iteration over `f` is equivalent to the CCPO
-fixpoint of `f` if there exists a CCPO making `f` monotone.
--/
-open _root_.Classical in
-/--
-A fixpoint combinator that can be used to construct recursive definitions with an *extrinsic*
-proof of monotonicity.
-
-Given a fixpoint functional {name}`f`, {lean}`extrinsicFix f` is the recursive function obtained
-by having {name}`f` call itself recursively.
-
-If there is no CCPO on `α` making {name}`f` monotone, {lean}`extrinsicFix f` might run forever.
-In this case, nothing interesting can be proved about the result; it is opaque.
-
-If there _is_ a CCPO on `α` making {name}`f` monotone, {lean}`extrinsicFix f` is equivalent to
-{lean}`CCPO.fix f`, logically and regarding its termination behavior.
--/
-@[cbv_opaque, implemented_by opaqueFix]
-def extrinsicFix {α : Sort u} [Nonempty α] (f : α → α) : α :=
-  if h : ∃ x, x = f x then
-    h.choose
-  else
-    -- Return `opaqueFix f` so that `implemented_by opaqueFix` is sound.
-    -- In effect, `extrinsicFix` is opaque if no fixpoint exists.
-    opaqueFix f
-
-/--
-A fixpoint combinator that allows for deferred proofs of monotonicity.
-
-{lean}`extrinsicFix f` is a function implemented as the loop
-{lean}`extrinsicFix f = f (extrinsicFix f)`.
-
-If there is a CCPO making `f` monotone, {name}`extrinsicFix_eq` proves that it satisfies the
-fixpoint equation, and {name}`extrinsicFix_induct` enables fixpoint induction.
-Otherwise, {lean}`extrinsicFix f` is opaque, i.e., it is impossible to prove nontrivial
-properties about it.
--/
-add_decl_doc extrinsicFix
-
-/-- Every CCPO has at least one element (the bottom element). -/
-noncomputable local instance CCPO.instNonempty [CCPO α] : Nonempty α := ⟨bot⟩
-
-/--
-The fixpoint equation for `extrinsicFix`: given a proof that the fixpoint exists, unfold
-`extrinsicFix`.
--/
-theorem extrinsicFix_eq {f : α → α}
-    (x : α) (h : x = f x) :
-    letI : Nonempty α := ⟨x⟩; extrinsicFix f = f (extrinsicFix f) := by
-  letI : Nonempty α := ⟨x⟩
-  have h : ∃ x, x = f x := ⟨x, h⟩
-  simp only [extrinsicFix, dif_pos h]
-  exact h.choose_spec
-
-/--
-The fixpoint equation for `extrinsicFix`: given a CCPO instance and monotonicity of `f`,
-{lean}`extrinsicFix f = f (extrinsicFix f)`.
--/
-theorem extrinsicFix_eq_mono [inst : CCPO α] {f : α → α}
-    (hf : monotone f) :
-    extrinsicFix f = f (extrinsicFix f) :=
-  extrinsicFix_eq (fix f hf) (fix_eq hf)
-
-abbrev discardR {C : α → Sort _} {R : α → α → Prop}
-    (f : ∀ a, (∀ a', R a' a → C a') → C a) : ((∀ a, C a) → (∀ a, C a)) :=
-  fun rec a => f a (fun a _ => rec a)
-
-theorem extrinsicFix_eq_wf {C : α → Sort _} [∀ a, Nonempty (C a)] {R : α → α → Prop}
-    {f : ∀ a, (∀ a', R a' a → C a') → C a} (h : WellFounded R) {a : α} :
-    extrinsicFix (discardR f) a = f a (fun a _ => extrinsicFix (discardR f) a) := by
-  suffices extrinsicFix (discardR f) = fun a => f a (fun a _ => extrinsicFix (discardR f) a) by
-    conv => lhs; rw [this]
-  apply extrinsicFix_eq (fun a => WellFounded.fix h f a) (funext fun a => (WellFounded.fix_eq h f a))
-
-end Lean.Order

src/Init/Internal/Order/MonadTail.lean

@@ -1,140 +0,0 @@
-/-
-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/While.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Init.Core
-public import Init.Internal.Order.ExtrinsicFix
 
 public section
 
@@ -22,38 +21,18 @@ namespace Lean
 inductive Loop where
   | mk
 
-open Lean.Order in
 @[inline]
-def Loop.forIn {β : Type u} {m : Type u → Type v} [Monad m]
-    (_ : Loop) (init : β) (f : Unit → β → m (ForInStep β)) : m β :=
-  haveI : Nonempty (β → m β) := ⟨fun b => pure b⟩
-  Lean.Order.extrinsicFix (fun (cont : β → m β) (b : β) => do
+partial def Loop.forIn {β : Type u} {m : Type u → Type v} [Monad m] (_ : Loop) (init : β) (f : Unit → β → m (ForInStep β)) : m β :=
+  let rec @[specialize] loop (b : β) : m β := do
     match ← f () b with
-    | .done val => pure val
-    | .yield val => cont val) init
+      | ForInStep.done b  => pure b
+      | ForInStep.yield b => loop b
+  loop init
 
 instance [Monad m] : ForIn m Loop Unit where
   forIn := Loop.forIn
 
-open Lean.Order in
-theorem Loop.forIn_eq [Monad m] [MonadTail m]
-    {l : Loop} {b : β} {f : Unit → β → m (ForInStep β)} :
-    Loop.forIn l b f = (do
-      match ← f () b with
-      | .done val => pure val
-      | .yield val => Loop.forIn l val f) := by
-  haveI : Nonempty β := ⟨b⟩
-  simp only [Loop.forIn]
-  apply congrFun
-  apply extrinsicFix_eq
-  intro cont₁ cont₂ h b'
-  apply MonadTail.bind_mono_right
-  intro r
-  cases r with
-  | done => exact PartialOrder.rel_refl
-  | yield val => exact h val
-
-syntax (name := doRepeat) "repeat " doSeq : doElem
+syntax "repeat " doSeq : doElem
 
 macro_rules
   | `(doElem| repeat $seq) => `(doElem| for _ in Loop.mk do $seq)

src/Lean/Compiler/LCNF/ExpandResetReuse.lean

@@ -90,6 +90,22 @@ partial def eraseProjIncFor (nFields : Nat) (targetId : FVarId) (ds : Array (Cod
         | break
       if !(w == z && targetId == x) then
         break
+      if mask[i]!.isSome then
+        /-
+        Suppose we encounter a situation like
+        ```
+        let x.1 := proj[0] y
+        inc x.1
+        let x.2 := proj[0] y
+        inc x.2
+        ```
+        The `inc x.2` will already have been removed. If we don't perform this check we will also
+        remove `inc x.1` and have effectively removed two refcounts while only one was legal.
+        -/
+        keep := keep.push d
+        keep := keep.push d'
+        ds := ds.pop.pop
+        continue
       /-
       Found
       ```

src/Lean/Elab/Do/Legacy.lean

@@ -1782,10 +1782,6 @@ 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/Inductive.lean

@@ -73,6 +73,8 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) (isCoi
         throwError "Constructor cannot be `protected` because it is in a `private` inductive datatype"
       checkValidCtorModifier ctorModifiers
       let ctorName := ctor.getIdAt 3
+      if ctorName.hasMacroScopes && isCoinductive then
+        throwError "Coinductive predicates are not allowed inside of macro scopes"
       let ctorName := declName ++ ctorName
       let ctorName ← withRef ctor[3] <| applyVisibility ctorModifiers ctorName
       let (binders, type?) := expandOptDeclSig ctor[4]

src/Std/Do/SPred/DerivedLaws.lean

@@ -178,48 +178,6 @@ 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
-
-@[simp, grind =] theorem evalsTo_3 {f : SVal [σ₁, σ₂, σ₃] α} {a : α}
-    {s₁ : σ₁} {s₂ : σ₂} {s₃ : σ₃} :
-    evalsTo f a s₁ s₂ s₃ = evalsTo (f s₁ s₂ s₃) a := rfl
-
-@[simp, grind =] theorem evalsTo_4 {f : SVal [σ₁, σ₂, σ₃, σ₄] α} {a : α}
-    {s₁ : σ₁} {s₂ : σ₂} {s₃ : σ₃} {s₄ : σ₄} :
-    evalsTo f a s₁ s₂ s₃ s₄ = evalsTo (f s₁ s₂ s₃ s₄) a := rfl
-
-@[simp, grind =] theorem evalsTo_5 {f : SVal [σ₁, σ₂, σ₃, σ₄, σ₅] α} {a : α}
-    {s₁ : σ₁} {s₂ : σ₂} {s₃ : σ₃} {s₄ : σ₄} {s₅ : σ₅} :
-    evalsTo f a s₁ s₂ s₃ s₄ s₅ = evalsTo (f s₁ s₂ s₃ 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
@@ -380,4 +338,3 @@ 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,7 +7,6 @@ module
 
 prelude
 public import Std.Do.SPred.Notation
-import Init.PropLemmas
 
 @[expose] public section
 
@@ -158,17 +157,3 @@ 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

@@ -1,94 +0,0 @@
-/-
-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 `Loop`-based `repeat`/`while` loops
-
-This file contains the `@[spec]` theorem for `forIn` over `Lean.Loop`, 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_loop
-    {l : _root_.Lean.Loop} {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.Loop.forIn_eq]
-  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,7 +10,6 @@ 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.While
 
 -- This public import is a workaround for #10652.
 -- Without it, adding the `spec` attribute for `instMonadLiftTOfMonadLift` will fail.

src/Std/Tactic/Do.lean

@@ -8,7 +8,6 @@ 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/13407.lean

@@ -0,0 +1,64 @@
+module
+
+/-! Regression test for issue 13407 -/
+
+inductive Result (α : Type) where | ok (x : α) | err
+instance : Monad Result where
+  pure x := .ok x
+  bind s f := match s with | .ok x => f x | .err => .err
+instance : Coe α (Result α) where coe x := .ok x
+
+structure Int' (bits : Nat) where val : Nat
+
+def Int'.wrap (n : Int) (bits : Nat) : Int' bits := ⟨(n % (2^bits : Int)).toNat⟩
+
+def Int'.toInt (x : Int' bits) : Int :=
+  if x.val < 2^(bits - 1) then ↑x.val else ↑x.val - ↑(2^bits)
+
+instance (n : Nat) : OfNat (Int' bits) n where ofNat := ⟨n % (2^bits)⟩
+instance : Neg (Int' bits) where neg x := Int'.wrap (-Int'.toInt x) bits
+instance : Repr (Int' bits) := ⟨fun x _ => repr (Int'.toInt x)⟩
+
+class BinOp1 (α β : Type) (γ : outParam Type) where binOp1 : α → β → γ
+class BinOp2 (α β : Type) (γ : outParam Type) where binOp2 : α → β → γ
+class UnaryOp (α : Type) (β : outParam Type) where unaryOp : α → β
+class Cast (α β : Type) where cast : α → Result β
+
+instance : BinOp1 (Int' b) (Int' b) (Result (Int' b)) where
+  binOp1 a c := .ok (Int'.wrap (a.toInt + c.toInt) b)
+
+instance : BinOp1 (Int' l) (Int' r) (Result (Int' l)) where
+  binOp1 a c := .ok (Int'.wrap (a.toInt + c.toInt) l)
+
+instance : BinOp2 (Int' b) (Int' b) (Result (Int' b)) where
+  binOp2 a c := .ok (Int'.wrap (a.toInt + c.toInt) b)
+
+instance : UnaryOp (Int' b) (Result (Int' b)) where
+  unaryOp a := .ok (Int'.wrap (-(a.toInt + 1)) b)
+
+instance : Cast (Int' n) (Int' m) where
+  cast x := .ok (Int'.wrap x.toInt m)
+
+set_option linter.unusedVariables false
+
+def helper (_ : Nat) : Result (Int' 64) := UnaryOp.unaryOp (1 : Int' 64)
+
+def test (a : Nat) : Result (Int' 16) := do
+  let x ← UnaryOp.unaryOp (1 : Int' 16)
+  let y ← BinOp2.binOp2
+        (← (Cast.cast (← helper a) : Result (Int' 128)))
+        (← BinOp1.binOp1
+              (← (Cast.cast (← helper a) : Result (Int' 128)))
+              (← BinOp2.binOp2
+                    (← BinOp1.binOp1 (10 : Int' 128) (1 : Int' 128))
+                    (← BinOp2.binOp2 (7 : Int' 128) (3 : Int' 128))))
+  BinOp1.binOp1
+    (← (Cast.cast (← (Cast.cast y : Result (Int' 128))) : Result (Int' 16)))
+    (← BinOp2.binOp2 x (← BinOp2.binOp2 x x))
+
+/-- info: 11 -/
+#guard_msgs in
+#eval do
+  match test 0 with
+  | .ok v => IO.println (repr v)
+  | .err => IO.println "ERR"

tests/elab/13415.lean

@@ -0,0 +1,13 @@
+macro "co " x:ident : command => do
+  `(coinductive $x : Prop where | ok)
+
+/-- error: Coinductive predicates are not allowed inside of macro scopes -/
+#guard_msgs in
+co f
+
+macro "co2" : command => do
+  `(coinductive test : Prop where | ctor)
+
+/-- error: Coinductive predicates are not allowed inside of macro scopes -/
+#guard_msgs in
+co2

tests/elab/repeat_extrinsic.lean

@@ -1,126 +0,0 @@
-module
-
-import Std
-
-set_option mvcgen.warning false
-
-open Std.Do
-
-/-!
-# Tests for `Loop`-based `repeat`/`while` loops with `extrinsicFix`
-
-These tests verify that the `Loop.forIn` implementation using `extrinsicFix` and its
-verification infrastructure work correctly 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
-
-def terminatesSometimes (n : Nat) (p : Nat → Bool) :  Option Nat := do
-  let mut n := n
-  while !p n do
-    n := n + 2
-  return n
-
-example (n m : Nat) (h : n ≤ m) (heven : n % 2 = 0) (hmeven : m % 2 = 0) (h : p m) :
-    ⦃⌜True⌝⦄ terminatesSometimes n p ⦃⇓ r => ⌜r % 2 = 0⌝⦄ := by
-  mvcgen [terminatesSometimes] invariants
-  | inv1 => fun i => ULift.up (m + 1 - i)
-  | inv2 => ⇓ (done, i) => ⌜i % 2 = 0 ∧ i ≤ m⌝ ∧ ⌜done = true → p i⌝
-  with grind