feat: Subarray.findRev?

src/Init/Data/Array/Subarray.lean

@@ -104,6 +104,28 @@ def any {α : Type u} (p : α → Bool) (as : Subarray α) : Bool :=
 def all {α : Type u} (p : α → Bool) (as : Subarray α) : Bool :=
   Id.run <| as.allM p
 
+@[inline]
+def findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Subarray α) (f : α → m (Option β)) : m (Option β) :=
+  let rec @[specialize] find : (i : Nat) → i ≤ as.size → m (Option β)
+    | 0,   _ => pure none
+    | i+1, h => do
+      have : i < as.size := Nat.lt_of_lt_of_le (Nat.lt_succ_self _) h
+      let r ← f as[i]
+      match r with
+      | some _ => pure r
+      | none   =>
+        have : i ≤ as.size := Nat.le_of_lt this
+        find i this
+  find as.size (Nat.le_refl _)
+
+@[inline]
+def findRevM? {α : Type} {m : Type → Type w} [Monad m] (as : Subarray α) (p : α → m Bool) : m (Option α) :=
+  as.findSomeRevM? fun a => return if (← p a) then some a else none
+
+@[inline]
+def findRev? {α : Type} (as : Subarray α) (p : α → Bool) : Option α :=
+  Id.run <| as.findRevM? p
+
 end Subarray
 
 namespace Array