From e044ffae6ab470080a00df92274449a46a4a6a98 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 4 Mar 2026 17:38:07 -0800 Subject: [PATCH] fix: mark `Id.run` as `[implicit_reducible]` (#12757) This PR marks `Id.run` as `[implicit_reducible]` to ensure that `Id.instMonadLiftTOfPure` and `instMonadLiftT Id` are definitionally equal when using `.implicitReducible` transparency setting. --- src/Init/Control/Id.lean | 2 +- src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/Control/Id.lean b/src/Init/Control/Id.lean index 300a99f273..8858236f77 100644 --- a/src/Init/Control/Id.lean +++ b/src/Init/Control/Id.lean @@ -58,7 +58,7 @@ Runs a computation in the identity monad. This function is the identity function. Because its parameter has type `Id α`, it causes `do`-notation in its arguments to use the `Monad Id` instance. -/ -@[always_inline, inline, expose] +@[always_inline, inline, expose, implicit_reducible] protected def run (x : Id α) : α := x instance [OfNat α n] : OfNat (Id α) n := diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean index 9b3f349823..c89d4e99ae 100644 --- a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean +++ b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean @@ -395,7 +395,7 @@ theorem Iter.fold_eq_fold_toIterM {α β : Type w} {γ : Type w} [Iterator α Id [Finite α Id] [IteratorLoop α Id Id] {f : γ → β → γ} {init : γ} {it : Iter (α := α) β} : it.fold (init := init) f = (it.toIterM.fold (init := init) f).run := by - rw [fold_eq_foldM, foldM_eq_foldM_toIterM, IterM.fold_eq_foldM]; rfl + rw [fold_eq_foldM, foldM_eq_foldM_toIterM, IterM.fold_eq_foldM] @[simp] theorem Iter.forIn_pure_yield_eq_fold {α β : Type w} {γ : Type x} [Iterator α Id β]