From 9371aa0e9975f888021d0971eb831dd6fdff6d33 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 18 Jun 2016 14:27:57 -0700
Subject: [PATCH] refactor(library/data/list/basic): move tail to init

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

diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean
index 5654a45cab..79ab6c4859 100644
--- a/library/data/list/basic.lean
+++ b/library/data/list/basic.lean
@@ -144,10 +144,6 @@ rfl
 theorem head_append [simp] [h : inhabited T] (t : list T) : ∀ {s : list T}, s ≠ [] → head (s ++ t) = head s :=
 sorry -- by rec_inst_simp
 
-definition tail : list T → list T
-| []       := []
-| (a :: l) := l
-
 theorem tail_nil [simp] : tail (@nil T) = [] :=
 rfl
 
diff --git a/library/init/list.lean b/library/init/list.lean
index 67fe278605..9cd8a9aecd 100644
--- a/library/init/list.lean
+++ b/library/init/list.lean
@@ -49,4 +49,8 @@ definition nth : list A → nat → option A
 | (a :: l) 0     := some a
 | (a :: l) (n+1) := nth l n
 
+definition tail : list A → list A
+| []       := []
+| (a :: l) := l
+
 end list