From 16aaa9b88ef79ec3b568e09cf99ea16a149444d0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Johannes=20H=C3=B6lzl?= <johannes.hoelzl@gmx.de>
Date: Mon, 20 Feb 2017 11:07:53 -0500
Subject: [PATCH] feat(library/init/data/list): add unzip

---
 library/init/data/list/basic.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/library/init/data/list/basic.lean b/library/init/data/list/basic.lean
index 88520498fb..3b08c7e087 100644
--- a/library/init/data/list/basic.lean
+++ b/library/init/data/list/basic.lean
@@ -167,6 +167,10 @@ def zip_with (f : α → β → γ) : list α → list β → list γ
 def zip : list α → list β → list (prod α β) :=
 zip_with prod.mk
 
+def unzip : list (α × β) → list α × list β
+| []            := ([], [])
+| ((a, b) :: t) := match unzip t with (al, bl) := (a::al, b::bl) end
+
 def repeat (a : α) : ℕ → list α
 | 0 := []
 | (succ n) := a :: repeat n