From 7f3e1705091ecf0b4534d2e274729d381a5bfe8e Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Mon, 10 Feb 2025 09:54:51 +1100
Subject: [PATCH] chore: unprotect List.foldlM (#7003)

---
 src/Init/Data/Array/Lemmas.lean | 2 +-
 src/Init/Data/List/Control.lean | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index 8d0de5c79f..caf0243a5f 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -3653,7 +3653,7 @@ theorem toListRev_toArray (l : List α) : l.toArray.toListRev = l.reverse := by
     l.toArray.mapM f = List.toArray <$> l.mapM f := by
   simp only [← mapM'_eq_mapM, mapM_eq_foldlM]
   suffices ∀ init : Array β,
-      foldlM (fun bs a => bs.push <$> f a) init l.toArray = (init ++ toArray ·) <$> mapM' f l by
+      Array.foldlM (fun bs a => bs.push <$> f a) init l.toArray = (init ++ toArray ·) <$> mapM' f l by
     simpa using this #[]
   intro init
   induction l generalizing init with
diff --git a/src/Init/Data/List/Control.lean b/src/Init/Data/List/Control.lean
index 91c224dc2e..fb00dfa491 100644
--- a/src/Init/Data/List/Control.lean
+++ b/src/Init/Data/List/Control.lean
@@ -161,7 +161,7 @@ foldlM f x₀ [a, b, c] = do
 ```
 -/
 @[specialize]
-protected def foldlM {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} : (f : s → α → m s) → (init : s) → List α → m s
+def foldlM {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} : (f : s → α → m s) → (init : s) → List α → m s
   | _, s, []      => pure s
   | f, s, a :: as => do
     let s' ← f s a