From 422820243dcce7da084e3ffbd2a816fe35d15f79 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Sat, 6 May 2017 03:00:43 -0400
Subject: [PATCH] chore(tools/super/utils): remove duplicate partition def

---
 library/tools/super/utils.lean | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/library/tools/super/utils.lean b/library/tools/super/utils.lean
index 647597f8fc..94cbb6f0d0 100644
--- a/library/tools/super/utils.lean
+++ b/library/tools/super/utils.lean
@@ -72,10 +72,6 @@ private def zip_with_index' {A} : ℕ → list A → list (A × ℕ)
 def zip_with_index {A} : list A → list (A × ℕ) :=
 zip_with_index' 0
 
-def partition {A} (pred : A → Prop) [decidable_pred pred] : list A → list A × list A
-| (x::xs) := match partition xs with (ts,fs) := if pred x then (x::ts, fs) else (ts, x::fs) end
-| [] := ([],[])
-
 meta def merge_sorted {A} [has_ordering A] : list A → list A → list A
 | [] ys := ys
 | xs [] := xs