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 /--