feat: add contains for List and Array

library/Init/Data/Array/Basic.lean

@@ -526,6 +526,9 @@ end
 def eraseIdx' {α} (a : Array α) (i : Fin a.size) : { r : Array α // r.size = a.size - 1 } :=
 eraseIdxSzAux a (i.val + 1) a rfl
 
+def contains [HasBeq α] (as : Array α) (a : α) : Bool :=
+as.any $ fun b => a == b
+
 end Array
 
 export Array (mkArray)

library/Init/Data/List/Basic.lean

@@ -168,6 +168,9 @@ def elem [HasBeq α] (a : α) : List α → Bool
 def notElem [HasBeq α] (a : α) (as : List α) : Bool :=
 !(as.elem a)
 
+abbrev contains [HasBeq α] (as : List α) (a : α) : Bool :=
+elem a as
+
 def eraseDupsAux {α} [HasBeq α] : List α → List α → List α
 | [],    bs => bs.reverse
 | a::as, bs => match bs.elem a with