refactor(library): list.taken/dropn ~> list.take/drop

library/data/bitvec.lean

@@ -36,7 +36,7 @@ section shift
 
   def shl (x : bitvec n) (i : ℕ) : bitvec n :=
   bitvec.cong (by simp) $
-    dropn i x ++ₜ repeat ff (min n i)
+    drop i x ++ₜ repeat ff (min n i)
 
   def fill_shr (x : bitvec n) (i : ℕ) (fill : bool) : bitvec n :=
   bitvec.cong
@@ -47,7 +47,7 @@ section shift
       { have h₁ := le_of_not_ge h,
         rw [min_eq_left h₁, sub_eq_zero_of_le h₁, min_zero_left, add_zero] }
     end $
-    repeat fill (min n i) ++ₜ taken (n-i) x
+    repeat fill (min n i) ++ₜ take (n-i) x
 
   -- unsigned shift right
   def ushr (x : bitvec n) (i : ℕ) : bitvec n :=

library/data/buffer.lean

@@ -90,14 +90,14 @@ def foldl : buffer α → β → (α → β → β) → β
 def rev_iterate : Π (b : buffer α), β → (fin b.size → α → β → β) → β
 | ⟨_, a⟩ b f := a.rev_iterate b f
 
-def taken (b : buffer α) (n : nat) : buffer α :=
-if h : n ≤ b.size then ⟨n, b.to_array.taken n h⟩ else b
+def take (b : buffer α) (n : nat) : buffer α :=
+if h : n ≤ b.size then ⟨n, b.to_array.take n h⟩ else b
 
-def taken_right (b : buffer α) (n : nat) : buffer α :=
-if h : n ≤ b.size then ⟨n, b.to_array.taken_right n h⟩ else b
+def take_right (b : buffer α) (n : nat) : buffer α :=
+if h : n ≤ b.size then ⟨n, b.to_array.take_right n h⟩ else b
 
-def dropn (b : buffer α) (n : nat) : buffer α :=
-if h : n ≤ b.size then ⟨_, b.to_array.dropn n h⟩ else b
+def drop (b : buffer α) (n : nat) : buffer α :=
+if h : n ≤ b.size then ⟨_, b.to_array.drop n h⟩ else b
 
 def reverse (b : buffer α) : buffer α :=
 ⟨b.size, b.to_array.reverse⟩

library/data/buffer/parser.lean

@@ -185,8 +185,8 @@ private def make_monospaced : char → char
 | c := c
 
 def mk_error_msg (input : char_buffer) (pos : ℕ) (expected : dlist string) : char_buffer :=
-let left_ctx := (input.taken pos).taken_right 10,
-    right_ctx := (input.dropn pos).taken 10 in
+let left_ctx := (input.take pos).take_right 10,
+    right_ctx := (input.drop pos).take 10 in
 left_ctx.map make_monospaced ++ right_ctx.map make_monospaced ++ "\n".to_char_buffer ++
 left_ctx.map (λ _, ' ') ++ "^\n".to_char_buffer ++
 "\n".to_char_buffer ++

library/data/vector.lean

@@ -76,11 +76,11 @@ def map₂ (f : α → β → φ) : vector α n → vector β n → vector φ n
 def repeat (a : α) (n : ℕ) : vector α n :=
 ⟨ list.repeat a n, list.length_repeat a n ⟩
 
-def dropn (i : ℕ) : vector α n → vector α (n - i)
-| ⟨l, p⟩ := ⟨ list.dropn i l, by simp * ⟩
+def drop (i : ℕ) : vector α n → vector α (n - i)
+| ⟨l, p⟩ := ⟨ list.drop i l, by simp * ⟩
 
-def taken (i : ℕ) : vector α n → vector α (min i n)
-| ⟨l, p⟩ := ⟨ list.taken i l, by simp * ⟩
+def take (i : ℕ) : vector α n → vector α (min i n)
+| ⟨l, p⟩ := ⟨ list.take i l, by simp * ⟩
 
 def remove_nth (i : fin n) : vector α n → vector α (n - 1)
 | ⟨l, p⟩ := ⟨ list.remove_nth l i.1, by rw[l.length_remove_nth i.1]; rw p; exact i.2 ⟩
@@ -126,10 +126,10 @@ begin cases v, reflexivity end
 @[simp] lemma to_list_append {n m : nat} (v : vector α n) (w : vector α m) : to_list (append v w) = to_list v ++ to_list w :=
 begin cases v, cases w, reflexivity end
 
-@[simp] lemma to_list_dropn {n m : ℕ} (v : vector α m) : to_list (dropn n v) = list.dropn n (to_list v) :=
+@[simp] lemma to_list_drop {n m : ℕ} (v : vector α m) : to_list (drop n v) = list.drop n (to_list v) :=
 begin cases v, reflexivity end
 
-@[simp] lemma to_list_taken {n m : ℕ} (v : vector α m) : to_list (taken n v) = list.taken n (to_list v) :=
+@[simp] lemma to_list_take {n m : ℕ} (v : vector α m) : to_list (take n v) = list.take n (to_list v) :=
 begin cases v, reflexivity end
 
 end vector

library/init/data/array/slice.lean

@@ -16,18 +16,18 @@ def slice (a : array α n) (k l : nat) (h₁ : k ≤ l) (h₂ : l ≤ n) : array
          ... = l : nat.sub_add_cancel h₁
          ... ≤ n : h₂⟩ ⟩
 
-def taken (a : array α n) (m : nat) (h : m ≤ n) : array α m :=
+def take (a : array α n) (m : nat) (h : m ≤ n) : array α m :=
 cast (by simp) $ a.slice 0 m (nat.zero_le _) h
 
-def dropn (a : array α n) (m : nat) (h : m ≤ n) : array α (n-m) :=
+def drop (a : array α n) (m : nat) (h : m ≤ n) : array α (n-m) :=
 a.slice m n h (le_refl _)
 
 private lemma sub_sub_cancel (m n : ℕ) (h : m ≤ n) : n - (n - m) = m :=
 calc n - (n - m) = (n - m) + m - (n - m) : by rw nat.sub_add_cancel; assumption
              ... = m : nat.add_sub_cancel_left _ _
 
-def taken_right (a : array α n) (m : nat) (h : m ≤ n) : array α m :=
-cast (by simp [*, sub_sub_cancel]) $ a.dropn (n - m) (nat.sub_le _ _)
+def take_right (a : array α n) (m : nat) (h : m ≤ n) : array α m :=
+cast (by simp [*, sub_sub_cancel]) $ a.drop (n - m) (nat.sub_le _ _)
 
 def reverse (a : array α n) : array α n :=
 ⟨ λ ⟨ i, hi ⟩, a.read ⟨ n - (i + 1),

library/init/data/list/basic.lean

@@ -182,15 +182,15 @@ def index_of [decidable_eq α] (a : α) : list α → nat := find_index (eq a)
 
 def indexes_of [decidable_eq α] (a : α) : list α → list nat := find_indexes (eq a)
 
-def dropn : ℕ → list α → list α
+def drop : ℕ → list α → list α
 | 0        a      := a
 | (succ n) []     := []
-| (succ n) (x::r) := dropn n r
+| (succ n) (x::r) := drop n r
 
-def taken : ℕ → list α → list α
+def take : ℕ → list α → list α
 | 0        a        := []
 | (succ n) []       := []
-| (succ n) (x :: r) := x :: taken n r
+| (succ n) (x :: r) := x :: take n r
 
 def split_at : ℕ → list α → list α × list α
 | 0        a         := ([], a)

library/init/data/list/instances.lean

@@ -113,13 +113,13 @@ instance decidable_suffix [decidable_eq α] : ∀ (l₁ l₂ : list α), decidab
                 append_ne_nil_of_ne_nil_right _ _ $ λh, list.no_confusion h
 | l₁      l₂ := let len1 := length l₁, len2 := length l₂ in
   if hl : len1 ≤ len2 then
-    if he : dropn (len2 - len1) l₂ = l₁ then is_true $
-      ⟨taken (len2 - len1) l₂, by rw [-he, taken_append_dropn]⟩
+    if he : drop (len2 - len1) l₂ = l₁ then is_true $
+      ⟨take (len2 - len1) l₂, by rw [-he, take_append_drop]⟩
     else is_false $
-      suffices length l₁ ≤ length l₂ → l₁ <:+ l₂ → dropn (length l₂ - length l₁) l₂ = l₁,
+      suffices length l₁ ≤ length l₂ → l₁ <:+ l₂ → drop (length l₂ - length l₁) l₂ = l₁,
         from λsuf, he (this hl suf),
       λ hl ⟨t, te⟩, and.right $
-        append_right_inj (eq.trans (taken_append_dropn (length l₂ - length l₁) l₂) te.symm) $
+        append_right_inj (eq.trans (take_append_drop (length l₂ - length l₁) l₂) te.symm) $
         by simp; exact nat.sub_sub_self hl
   else is_false $ λ⟨t, te⟩, hl $
     show length l₁ ≤ length l₂, by rw [-te, length_append]; apply nat.le_add_left

library/init/data/list/lemmas.lean

@@ -57,19 +57,19 @@ by {induction l, contradiction, simp}
 @[simp] lemma length_tail (l : list α) : length (tail l) = length l - 1 :=
 by cases l; refl
 
-/- repeat taken dropn -/
+/- repeat take drop -/
 
-attribute [simp] repeat taken dropn
+attribute [simp] repeat take drop
 
-@[simp] lemma split_at_eq_taken_dropn : ∀ (n : ℕ) (l : list α), split_at n l = (taken n l, dropn n l)
+@[simp] lemma split_at_eq_take_drop : ∀ (n : ℕ) (l : list α), split_at n l = (take n l, drop n l)
 | 0        a         := rfl
 | (succ n) []        := rfl
-| (succ n) (x :: xs) := by simp [split_at, split_at_eq_taken_dropn n xs]
+| (succ n) (x :: xs) := by simp [split_at, split_at_eq_take_drop n xs]
 
-@[simp] lemma taken_append_dropn : ∀ (n : ℕ) (l : list α), taken n l ++ dropn n l = l
+@[simp] lemma take_append_drop : ∀ (n : ℕ) (l : list α), take n l ++ drop n l = l
 | 0        a         := rfl
 | (succ n) []        := rfl
-| (succ n) (x :: xs) := by simp [taken_append_dropn n xs]
+| (succ n) (x :: xs) := by simp [take_append_drop n xs]
 
 /- length -/
 
@@ -94,18 +94,18 @@ lemma ne_nil_of_length_eq_succ {l : list α} : ∀ {n : nat}, length l = succ n
 by induction l; intros; contradiction
 
 -- TODO(Leo): cleanup proof after arith dec proc
-@[simp] lemma length_taken : ∀ (i : ℕ) (l : list α), length (taken i l) = min i (length l)
+@[simp] lemma length_take : ∀ (i : ℕ) (l : list α), length (take i l) = min i (length l)
 | 0        l      := by simp
 | (succ n) []     := by simp
 | (succ n) (a::l) := begin simp [*, nat.min_succ_succ, add_one_eq_succ] end
 
 -- TODO(Leo): cleanup proof after arith dec proc
-@[simp] lemma length_dropn : ∀ (i : ℕ) (l : list α), length (dropn i l) = length l - i
+@[simp] lemma length_drop : ∀ (i : ℕ) (l : list α), length (drop i l) = length l - i
 | 0 l         := rfl
 | (succ i) [] := eq.symm (nat.zero_sub_eq_zero (succ i))
 | (succ i) (x::l) := calc
-  length (dropn (succ i) (x::l))
-          = length l - i             : length_dropn i l
+  length (drop (succ i) (x::l))
+          = length l - i             : length_drop i l
       ... = succ (length l) - succ i : nat.sub_eq_succ_sub_succ (length l) i
 
 lemma length_remove_nth : ∀ (l : list α) (i : ℕ), i < length l → length (remove_nth l i) = length l - 1
@@ -627,7 +627,7 @@ by simp [scanr]
 
 /- filter, partition, take_while, drop_while, span -/
 
-attribute [simp] repeat taken dropn
+attribute [simp] repeat take drop
 
 @[simp] lemma partition_eq_filter_filter (p : α → Prop) [decidable_pred p] : ∀ (l : list α), partition p l = (filter p l, filter (not ∘ p) l)
 | []     := rfl

library/init/data/string/basic.lean

@@ -48,7 +48,7 @@ def pop_back : string → string
 | ⟨s⟩ := ⟨s.tail⟩
 
 def popn_back : string → nat → string
-| ⟨s⟩ n := ⟨s.dropn n⟩
+| ⟨s⟩ n := ⟨s.drop n⟩
 
 def intercalate (s : string) (ss : list string) : string :=
 (list.intercalate s.to_list (ss.map to_list)).as_string
@@ -64,7 +64,7 @@ def back : string → char
 | ⟨c::cs⟩ := c
 
 def backn : string → nat → string
-| ⟨s⟩ n := ⟨s.taken n⟩
+| ⟨s⟩ n := ⟨s.take n⟩
 
 def join (l : list string) : string :=
 l.foldl (λ r s, r ++ s) ""

library/init/meta/coinductive_predicates.lean

@@ -106,7 +106,7 @@ private meta def elim_gen_sum_aux : nat → expr → list expr → tactic (list
 meta def elim_gen_sum (n : nat) (e : expr) : tactic (list expr) := do
   (hs, h') ← elim_gen_sum_aux n e [],
   gs ← get_goals,
-  set_goals $ (gs.taken (n+1)).reverse ++ gs.dropn (n+1),
+  set_goals $ (gs.take (n+1)).reverse ++ gs.drop (n+1),
   return $ hs.reverse ++ [h']
 
 end tactic

library/init/native/default.lean

@@ -215,7 +215,7 @@ meta def compile_call (head : name) (arity : nat) (args : list ir.expr) : ir_com
   then mk_call head args
   else if list.length args < arity
   then mk_under_sat_call head args
-  else mk_over_sat_call head (list.taken arity args) (list.dropn arity args)
+  else mk_over_sat_call head (list.take arity args) (list.drop arity args)
 
 meta def mk_object (arity : unsigned) (args : list ir.expr) : ir_compiler ir.expr :=
   let args'' := list.map assert_name args

tests/lean/run/mk_byte.lean

@@ -8,12 +8,12 @@ def byte_type := bitvec 8
 def mk_byte (a b : bool) (l : bitvec 6) : byte_type := a :: b :: l
 
 -- Get the third component
-def get_data (byte : byte_type) : bitvec 6 := vector.dropn 2 byte
+def get_data (byte : byte_type) : bitvec 6 := vector.drop 2 byte
 
 lemma get_data_mk_byte {a b : bool} {l : bitvec 6} : get_data (mk_byte a b l) = l :=
 begin
   apply vector.eq,
   unfold mk_byte,
   unfold get_data,
-  simp [to_list_dropn, to_list_cons, list.dropn]
+  simp [to_list_drop, to_list_cons, list.drop]
 end