From 26bc1602a7ff9365b8fe2bc8cbc7ac46cb634352 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 9 Jul 2016 17:23:28 -0700
Subject: [PATCH] refactor(library): move 'filter' to init folder

---
 library/data/list/comb.lean | 4 ----
 library/init/list.lean      | 4 ++++
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/library/data/list/comb.lean b/library/data/list/comb.lean
index 12120bb764..f14c7731e3 100644
--- a/library/data/list/comb.lean
+++ b/library/data/list/comb.lean
@@ -132,10 +132,6 @@ theorem length_map₂ : ∀(f : A → B → C) x y, length (map₂ f x y) = min
       ... = min (length (xh::xr)) (length (yh::yr))   : rfl
 
 /- filter -/
-definition filter (p : A → Prop) [h : decidable_pred p] : list A → list A
-| []     := []
-| (a::l) := if p a then a :: filter l else filter l
-
 theorem filter_nil [simp] (p : A → Prop) [h : decidable_pred p] : filter p [] = [] := rfl
 
 theorem filter_cons_of_pos [simp] {p : A → Prop} [h : decidable_pred p] {a : A} : ∀ l, p a → filter p (a::l) = a :: filter p l :=
diff --git a/library/init/list.lean b/library/init/list.lean
index 4e00d9be69..183cedcc4b 100644
--- a/library/init/list.lean
+++ b/library/init/list.lean
@@ -65,6 +65,10 @@ definition map {B : Type} (f : A → B) : list A → list B
 definition join : list (list A) → list A
 | []        := []
 | (l :: ls) := append l (join ls)
+
+definition filter (p : A → Prop) [h : decidable_pred p] : list A → list A
+| []     := []
+| (a::l) := if p a then a :: filter l else filter l
 end list
 
 definition list_has_append [instance] {A : Type} : has_append (list A) :=