From 4d2647f9c712db892e41e4ddaa64730628e82a11 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Tue, 23 Dec 2025 11:29:20 +0100 Subject: [PATCH] fix: foldlM mismatch part 2 (#11779) This PR fixes an oversight in the initial #11772 PR. Closes #11778. --- src/Init/Data/Array/Basic.lean | 4 +++- src/Init/Data/ByteArray/Basic.lean | 4 +++- src/Init/Data/FloatArray/Basic.lean | 4 +++- tests/lean/run/11778.lean | 11 +++++++++++ 4 files changed, 20 insertions(+), 3 deletions(-) create mode 100644 tests/lean/run/11778.lean diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 84f8e29e3c..2d5baf7b89 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -589,8 +589,10 @@ unsafe def foldlMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Mon if start < stop then if stop ≤ as.size then fold (USize.ofNat start) (USize.ofNat stop) init - else + else if start < as.size then fold (USize.ofNat start) (USize.ofNat as.size) init + else + pure init else pure init diff --git a/src/Init/Data/ByteArray/Basic.lean b/src/Init/Data/ByteArray/Basic.lean index a1b5cbb7a7..32f11f7e80 100644 --- a/src/Init/Data/ByteArray/Basic.lean +++ b/src/Init/Data/ByteArray/Basic.lean @@ -269,8 +269,10 @@ unsafe def foldlMUnsafe {β : Type v} {m : Type v → Type w} [Monad m] (f : β if start < stop then if stop ≤ as.size then fold (USize.ofNat start) (USize.ofNat stop) init - else + else if start < as.size then fold (USize.ofNat start) (USize.ofNat as.size) init + else + pure init else pure init diff --git a/src/Init/Data/FloatArray/Basic.lean b/src/Init/Data/FloatArray/Basic.lean index bfcde6fe83..71d91e9ba9 100644 --- a/src/Init/Data/FloatArray/Basic.lean +++ b/src/Init/Data/FloatArray/Basic.lean @@ -144,8 +144,10 @@ unsafe def foldlMUnsafe {β : Type v} {m : Type v → Type w} [Monad m] (f : β if start < stop then if stop ≤ as.size then fold (USize.ofNat start) (USize.ofNat stop) init - else + else if start < as.size then fold (USize.ofNat start) (USize.ofNat as.size) init + else + pure init else pure init diff --git a/tests/lean/run/11778.lean b/tests/lean/run/11778.lean new file mode 100644 index 0000000000..7c4a0921b4 --- /dev/null +++ b/tests/lean/run/11778.lean @@ -0,0 +1,11 @@ +/-- info: 0 -/ +#guard_msgs in +#eval Array.foldl (·+·) 0 #[1,2,3] (start := 5) (stop := 10) + +/-- info: 0 -/ +#guard_msgs in +#eval ByteArray.foldl (·+·) 0 ⟨#[1,2,3]⟩ (start := 5) (stop := 10) + +/-- info: 0.000000 -/ +#guard_msgs in +#eval FloatArray.foldl (·+·) 0 ⟨#[1,2,3]⟩ (start := 5) (stop := 10)