From 19e341cfcc3dfdd4fb9bd63fac428e7e8474da26 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 2 Aug 2019 11:06:20 -0700
Subject: [PATCH] feat(library/init/data/array/basic): add `Array.indexOf` and
 `Array.eraseIdx`

---
 library/init/data/array/basic.lean | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)

diff --git a/library/init/data/array/basic.lean b/library/init/data/array/basic.lean
index e1eedeebc2..973baf6a10 100644
--- a/library/init/data/array/basic.lean
+++ b/library/init/data/array/basic.lean
@@ -424,6 +424,32 @@ reverseAux a 0
 @[inline] def filter (p : α → Bool) (as : Array α) : Array α :=
 filterAux p as 0 0
 
+partial def indexOfAux {α} [HasBeq α] (a : Array α) (v : α) : Nat → Option (Fin a.size)
+| i :=
+  if h : i < a.size then
+    let idx : Fin a.size := ⟨i, h⟩;
+    if a.fget idx == v then some idx
+    else indexOfAux (i+1)
+  else none
+
+def indexOf {α} [HasBeq α] (a : Array α) (v : α) : Option (Fin a.size) :=
+indexOfAux a v 0
+
+partial def eraseIdxAux {α} : Nat → Array α → Array α
+| i a :=
+  if h : i < a.size then
+    let idx  : Fin a.size := ⟨i, h⟩;
+    let idx1 : Fin a.size := ⟨i - 1, Nat.ltOfLeOfLt (Nat.predLe i) h⟩;
+    eraseIdxAux (i+1) (a.fswap idx idx1)
+  else
+    a.pop
+
+def feraseIdx {α} (a : Array α) (i : Fin a.size) : Array α :=
+eraseIdxAux (i.val + 1) a
+
+def eraseIdx {α} (a : Array α) (i : Nat) : Array α :=
+if i < a.size then eraseIdxAux (i+1) a else a
+
 end Array
 
 export Array (mkArray)