From ea09ffc8ceb392ca0e12a285dc85d4f89819f4a0 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Wed, 6 Aug 2025 16:15:54 +0200
Subject: [PATCH] refactor: restore `Subarray.foldl` and `Subarray.forIn`
 signatures (#9762)

This PR does what #9234 regrettably failed to do: actually reintroduce
the signatures of some `Subarray` functions that are now implemented via
slices (see #9017) in order to ensure backward compatibility and
consistency. With this PR, the old interface is restored. As an added
benefit, `Subarray.forIn` is no longer opaque.
---
 src/Init/Data/Slice/Array/Iterator.lean | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/Init/Data/Slice/Array/Iterator.lean b/src/Init/Data/Slice/Array/Iterator.lean
index 40ab655ee0..d03d5204aa 100644
--- a/src/Init/Data/Slice/Array/Iterator.lean
+++ b/src/Init/Data/Slice/Array/Iterator.lean
@@ -108,9 +108,17 @@ Examples:
  * `#["red", "green", "blue"].toSubarray.popFront.foldl (· + ·.length) 0 = 9`
 -/
 @[inline]
-def foldl {α : Type u} {β : Type v} (f : β → α → β) (init : β) (as : Subarray α) : β :=
+def Subarray.foldl {α : Type u} {β : Type v} (f : β → α → β) (init : β) (as : Subarray α) : β :=
   Slice.foldl f (init := init) as
 
+/--
+The implementation of `ForIn.forIn` for `Subarray`, which allows it to be used with `for` loops in
+`do`-notation.
+-/
+@[inline]
+def Subarray.forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (s : Subarray α) (b : β) (f : α → β → m (ForInStep β)) : m β :=
+  ForIn.forIn s b f
+
 namespace Array
 
 /--