From 79c0833d062ca1cb95444a7336900ac28752a4cd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 14 Nov 2019 09:51:50 -0800
Subject: [PATCH] feat: add `contains` for `List` and `Array`

---
 library/Init/Data/Array/Basic.lean | 3 +++
 library/Init/Data/List/Basic.lean  | 3 +++
 2 files changed, 6 insertions(+)

diff --git a/library/Init/Data/Array/Basic.lean b/library/Init/Data/Array/Basic.lean
index 6d4bd6bb4d..07b795dbda 100644
--- a/library/Init/Data/Array/Basic.lean
+++ b/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)
diff --git a/library/Init/Data/List/Basic.lean b/library/Init/Data/List/Basic.lean
index c973d74729..2db35a723b 100644
--- a/library/Init/Data/List/Basic.lean
+++ b/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