fix: implementation of Array.anyMUnsafe

move test

Author: kim-em

src/Init/Data/Array/Basic.lean

@@ -328,8 +328,9 @@ unsafe def anyMUnsafe {α : Type u} {m : Type → Type w} [Monad m] (p : α →
       else
         any (i+1) stop
   if start < stop then
-    if stop ≤ as.size then
-      any (USize.ofNat start) (USize.ofNat stop)
+    let stop' := min stop as.size
+    if start < stop' then
+      any (USize.ofNat start) (USize.ofNat stop')
     else
       pure false
   else

tests/lean/run/1921.lean

@@ -0,0 +1,9 @@
+@[simp] theorem Array.size_singleton : #[a].size = 1 := rfl
+@[simp] theorem USize.not_size_le_one : ¬ USize.size ≤ 1 := by cases usize_size_eq <;> simp_all
+
+def f := #[true].any id 0 USize.size
+
+-- `native_decide` used to prove `false` here, due to a bug in `Array.anyMUnsafe`.
+example : f = true := by native_decide
+
+example : f = true := by simp [f, Array.any, Array.anyM]