From 7089762cd6c883dfc3757839db42792cc7f72e9d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 18 Jun 2016 12:40:00 -0700
Subject: [PATCH] refactor(library/data/list): move nth to init

---
 library/data/list/basic.lean | 5 -----
 library/init/list.lean       | 9 ++++++++-
 2 files changed, 8 insertions(+), 6 deletions(-)

diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean
index ded9ea279e..5654a45cab 100644
--- a/library/data/list/basic.lean
+++ b/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
 
diff --git a/library/init/list.lean b/library/init/list.lean
index 73ace3e8a6..67fe278605 100644
--- a/library/init/list.lean
+++ b/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