refactor(library/data/list/basic): move tail to init

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
 

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