From 641ccbc84669c99456f95dfc798594016c08e762 Mon Sep 17 00:00:00 2001
From: Joe Hendrix <jhendrix@galois.com>
Date: Wed, 25 Jan 2017 12:24:16 -0800
Subject: [PATCH] chore(library/data): remove (list/tuple).firstn in favor of
 taken

---
 library/data/bitvec.lean     |  2 +-
 library/data/list/basic.lean | 27 ++++++++++-----------------
 library/data/tuple.lean      |  4 ++--
 3 files changed, 13 insertions(+), 20 deletions(-)

diff --git a/library/data/bitvec.lean b/library/data/bitvec.lean
index 2cc1a1d79b..32fd6917b4 100644
--- a/library/data/bitvec.lean
+++ b/library/data/bitvec.lean
@@ -41,7 +41,7 @@ section shift
   local attribute [ematch] nat.add_sub_assoc sub_le le_of_not_ge sub_eq_zero_of_le
   def fill_shr (x : bitvec n) (i : ℕ) (fill : bool) : bitvec n :=
   bitvec.cong (begin [smt] by_cases (i ≤ n), eblast end) $
-    repeat fill (min n i) ++ₜ firstn (n-i) x
+    repeat fill (min n i) ++ taken (n-i) x
 
   -- unsigned shift right
   def ushr (x : bitvec n) (i : ℕ) : bitvec n :=
diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean
index 5881e06828..a97e097329 100644
--- a/library/data/list/basic.lean
+++ b/library/data/list/basic.lean
@@ -29,6 +29,16 @@ theorem length_concat (a : α) : ∀ (l : list α), length (concat l a) = succ (
   | nil := rfl
   | (cons b l) := congr_arg succ (length_concat l)
 
+@[simp]
+theorem length_taken
+: ∀ (i : ℕ) (l : list α), length (taken i l) = min i (length l)
+| 0        l      := eq.symm (nat.zero_min (length l))
+| (succ n) []     := eq.symm (nat.min_zero (succ n))
+| (succ n) (a::l) :=
+  calc succ (length (taken n l)) = succ (min n (length l)) : congr_arg succ (length_taken n l)
+                             ... = min (succ n) (succ (length l))
+                                     : eq.symm (nat.min_succ_succ  n (length l))
+
 @[simp]
 theorem length_dropn
 : ∀ (i : ℕ) (l : list α), length (dropn i l) = length l - i
@@ -49,21 +59,4 @@ theorem length_repeat (a : α) : ∀ (n : ℕ), length (repeat a n) = n
   | 0 := eq.refl 0
   | (succ i) := congr_arg succ (length_repeat i)
 
-/- firstn -/
-
-def firstn : ℕ → list α → list α
-| 0 l             := []
-| (succ n) []     := []
-| (succ n) (a::l) := a :: firstn n l
-
-@[simp]
-theorem length_firstn
-: ∀ (i : ℕ) (l : list α), length (firstn i l) = min i (length l)
-| 0        l      := eq.symm (nat.zero_min (length l))
-| (succ n) []     := eq.symm (nat.min_zero (succ n))
-| (succ n) (a::l) :=
-  calc succ (length (firstn n l)) = succ (min n (length l)) : congr_arg succ (length_firstn n l)
-                              ... = min (succ n) (succ (length l))
-                                     : eq.symm (nat.min_succ_succ  n (length l))
-
 end list
diff --git a/library/data/tuple.lean b/library/data/tuple.lean
index 11c5798563..891eca8a8d 100644
--- a/library/data/tuple.lean
+++ b/library/data/tuple.lean
@@ -69,8 +69,8 @@ def repeat (a : α) (n : ℕ) : tuple α n :=
 def dropn (i : ℕ) : tuple α n → tuple α (n - i)
 | ⟨l, p⟩ := ⟨ list.dropn i l, by simp_using_hs ⟩
 
-def firstn (i : ℕ) : tuple α n → tuple α (min i n)
-| ⟨l, p⟩ := ⟨ list.firstn i l, by simp_using_hs ⟩
+def taken (i : ℕ) : tuple α n → tuple α (min i n)
+| ⟨l, p⟩ := ⟨ list.taken i l, by simp_using_hs ⟩
 
 section accum
   open prod