From 4f3fd2cba6103c3e49e61371fbff286ac6ac62bd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 17 Feb 2017 20:58:17 -0800
Subject: [PATCH] feat(library/init/data/list/qsort): add temp qsort as meta
 definition

---
 library/init/data/list/default.lean |  2 +-
 library/init/data/list/qsort.lean   | 23 +++++++++++++++++++++++
 2 files changed, 24 insertions(+), 1 deletion(-)
 create mode 100644 library/init/data/list/qsort.lean

diff --git a/library/init/data/list/default.lean b/library/init/data/list/default.lean
index 07e3d69e15..c96488d952 100644
--- a/library/init/data/list/default.lean
+++ b/library/init/data/list/default.lean
@@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.list.basic init.data.list.instances init.data.list.lemmas
+import init.data.list.basic init.data.list.instances init.data.list.lemmas init.data.list.qsort
diff --git a/library/init/data/list/qsort.lean b/library/init/data/list/qsort.lean
new file mode 100644
index 0000000000..7e434fd7a9
--- /dev/null
+++ b/library/init/data/list/qsort.lean
@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura
+-/
+prelude
+import init.data.list.basic
+
+namespace list
+
+/- TODO(Leo): remove meta as soon as equation compiler has support for well founded recursion.
+
+   This is based on the minimalist Haskell "quicksort".
+
+   Remark: this is *not* really quicksort since it doesn't partition the elements in-place -/
+meta def qsort {α} (lt : α → α → bool) : list α → list α
+| []     := []
+| (h::t) :=
+  let small := filter (λ x, lt h x = ff) t,
+      large := filter (λ x, lt h x = tt) t
+  in qsort small ++ h :: qsort large
+
+end list