From 7410d0067850ce9849cee67731e92a12802957ae Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 10 Nov 2022 11:03:32 +0100
Subject: [PATCH] feat: Subarray.findRev?

---
 src/Init/Data/Array/Subarray.lean | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/src/Init/Data/Array/Subarray.lean b/src/Init/Data/Array/Subarray.lean
index 5dc905b810..6dc9525ac5 100644
--- a/src/Init/Data/Array/Subarray.lean
+++ b/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