refactor(library/data/list): move nth to init

library/data/list/basic.lean

@@ -447,11 +447,6 @@ end
 
 /- nth element -/
 section nth
-definition nth : list T → nat → option T
-| []       n     := none
-| (a :: l) 0     := some a
-| (a :: l) (n+1) := nth l n
-
 theorem nth_zero [simp] (a : T) (l : list T) : nth (a :: l) 0 = some a :=
 rfl
 

library/init/list.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import init.logic
+import init.logic init.nat
 open decidable list
 
 protected definition list.is_inhabited [instance] (A : Type) : inhabited (list A) :=
@@ -42,4 +42,11 @@ definition length : list A → nat
 | []       := 0
 | (a :: l) := length l + 1
 
+open option nat
+
+definition nth : list A → nat → option A
+| [] _           := none
+| (a :: l) 0     := some a
+| (a :: l) (n+1) := nth l n
+
 end list