{"count": 30, "header": "Found 30 declarations whose name contains \"List.replicate\".\n", "heartbeats": 0, "hits": [{"doc": "Creates a list that contains `n` copies of `a`.\n\n* `List.replicate 5 \"five\" = [\"five\", \"five\", \"five\", \"five\", \"five\"]`\n* `List.replicate 0 \"zero\" = []`\n* `List.replicate 2 ' ' = [' ', ' ']`\n", "module": "Init.Data.List.Basic", "name": "List.replicate", "type": " {\u03b1 : Type u} (n : \u2115) (a : \u03b1) : List \u03b1"}, {"doc": "Creates a list that contains `n` copies of `a`.\n\nThis is a tail-recursive version of `List.replicate`.\n\n* `List.replicateTR 5 \"five\" = [\"five\", \"five\", \"five\", \"five\", \"five\"]`\n* `List.replicateTR 0 \"zero\" = []`\n* `List.replicateTR 2 ' ' = [' ', ' ']`\n", "module": "Init.Data.List.Basic", "name": "List.replicateTR", "type": " {\u03b1 : Type u} (n : \u2115) (a : \u03b1) : List \u03b1"}, {"doc": null, "module": "Init.Data.List.Basic", "name": "List.replicateTR.loop", "type": " {\u03b1 : Type u} (a : \u03b1) : \u2115 \u2192 List \u03b1 \u2192 List \u03b1"}, {"doc": null, "module": "Init.Data.List.Basic", "name": "List.replicate_eq_replicateTR", "type": " : @List.replicate = @List.replicateTR"}, {"doc": null, "module": "Init.Data.List.Basic", "name": "List.replicate_zero", "type": " {\u03b1 : Type u} {a : \u03b1} : List.replicate 0 a = []"}, {"doc": null, "module": "Init.Data.List.Basic", "name": "List.replicateTR_loop_replicate_eq", "type": " {\u03b1 : Type u} {a : \u03b1} {m n : \u2115} : List.replicateTR.loop a n (List.replicate m a) = List.replicate (n + m) a"}, {"doc": null, "module": "Init.Data.List.Basic", "name": "List.replicate_succ", "type": " {\u03b1 : Type u} {a : \u03b1} {n : \u2115} : List.replicate (n + 1) a = a :: List.replicate n a"}, {"doc": null, "module": "Init.Data.List.Basic", "name": "List.replicateTR_loop_eq", "type": " {\u03b1\u271d : Type u_1} {a : \u03b1\u271d} {acc : List \u03b1\u271d} (n : \u2115) : List.replicateTR.loop a n acc = List.replicate n a ++ acc"}, {"doc": null, "module": "Init.Data.List.Lemmas", "name": "List.replicate_one", "type": " {\u03b1\u271d : Type u_1} {a : \u03b1\u271d} : List.replicate 1 a = [a]"}, {"doc": null, "module": "Init.Data.List.Lemmas", "name": "List.replicate_eq_nil_iff", "type": " {\u03b1 : Type u_1} {n : \u2115} (a : \u03b1) : List.replicate n a = [] \u2194 n = 0"}, {"doc": null, "module": "Init.Data.List.Lemmas", "name": "List.replicate_succ_ne_nil", "type": " {\u03b1 : Type u_1} {n : \u2115} {a : \u03b1} : List.replicate (n + 1) a \u2260 []"}, {"doc": null, "module": "Init.Data.List.Lemmas", "name": "List.replicate_inj", "type": " {n : \u2115} {\u03b1\u271d : Type u_1} {a : \u03b1\u271d} {m : \u2115} {b : \u03b1\u271d} : List.replicate n a = List.replicate m b \u2194 n = m \u2227 (n = 0 \u2228 a = b)"}, {"doc": null, "module": "Init.Data.List.Lemmas", "name": "List.replicate_append_replicate", "type": " {n : \u2115} {\u03b1\u271d : Type u_1} {a : \u03b1\u271d} {m : \u2115} : List.replicate n a ++ List.replicate m a = List.replicate (n + m) a"}, {"doc": null, "module": "Init.Data.List.Lemmas", "name": "List.replicate_beq_replicate", "type": " {\u03b1 : Type u_1} [BEq \u03b1] {a b : \u03b1} {n : \u2115} : (List.replicate n a == List.replicate n b) = (n == 0 || a == b)"}, {"doc": "Variant of `replicate_succ` that concatenates `a` to the end of the list. ", "module": "Init.Data.List.Lemmas", "name": "List.replicate_succ'", "type": " {n : \u2115} {\u03b1\u271d : Type u_1} {a : \u03b1\u271d} : List.replicate (n + 1) a = List.replicate n a ++ [a]"}, {"doc": null, "module": "Init.Data.List.Lemmas", "name": "List.replicate_eq_append_iff", "type": " {\u03b1 : Type u_1} {n : \u2115} {l\u2081 l\u2082 : List \u03b1} {a : \u03b1} : List.replicate n a = l\u2081 ++ l\u2082 \u2194 l\u2081.length + l\u2082.length = n \u2227 l\u2081 = List.replicate l\u2081.length a \u2227 l\u2082 = List.replicate l\u2082.length a"}, {"doc": "An induction principle for lists based on contiguous runs of identical elements. ", "module": "Init.Data.List.Lemmas", "name": "List.replicateRecOn", "type": " {\u03b1 : Type u_1} {p : List \u03b1 \u2192 Prop} (l : List \u03b1) (h0 : p []) (hr : \u2200 (a : \u03b1) (n : \u2115), 0 < n \u2192 p (List.replicate n a)) (hi : \u2200 (a b : \u03b1) (n : \u2115) (l : List \u03b1), a \u2260 b \u2192 0 < n \u2192 p (b :: l) \u2192 p (List.replicate n a ++ b :: l)) : p l"}, {"doc": null, "module": "Init.Data.List.Sublist", "name": "List.replicate_sublist_replicate", "type": " {\u03b1 : Type u_1} {m n : \u2115} (a : \u03b1) : (List.replicate m a).Sublist (List.replicate n a) \u2194 m \u2264 n"}, {"doc": null, "module": "Init.Data.List.Sublist", "name": "List.replicate_subset", "type": " {\u03b1 : Type u_1} {n : \u2115} {a : \u03b1} {l : List \u03b1} : List.replicate n a \u2286 l \u2194 n = 0 \u2228 a \u2208 l"}, {"doc": null, "module": "Init.Data.List.Count", "name": "List.replicate_sublist_iff", "type": " {\u03b1 : Type u_1} [BEq \u03b1] [LawfulBEq \u03b1] {n : \u2115} {a : \u03b1} {l : List \u03b1} : (List.replicate n a).Sublist l \u2194 n \u2264 List.count a l"}, {"doc": null, "module": "Init.Data.List.Count", "name": "List.replicate_count_eq_of_count_eq_length", "type": " {\u03b1 : Type u_1} [BEq \u03b1] [LawfulBEq \u03b1] {a : \u03b1} {l : List \u03b1} (h : List.count a l = l.length) : List.replicate (List.count a l) a = l"}, {"doc": null, "module": "Init.Data.List.Perm", "name": "List.replicate_perm", "type": " {\u03b1 : Type u_1} {n : \u2115} {a : \u03b1} {l : List \u03b1} : (List.replicate n a).Perm l \u2194 List.replicate n a = l"}, {"doc": null, "module": "Mathlib.Data.List.Basic", "name": "List.replicate_left_injective", "type": " {\u03b1 : Type u} (a : \u03b1) : Function.Injective fun x => List.replicate x a"}, {"doc": null, "module": "Mathlib.Data.List.Basic", "name": "List.replicate_right_injective", "type": " {\u03b1 : Type u} {n : \u2115} (hn : n \u2260 0) : Function.Injective (List.replicate n)"}, {"doc": null, "module": "Mathlib.Data.List.Basic", "name": "List.replicate_subset_singleton", "type": " {\u03b1 : Type u} (n : \u2115) (a : \u03b1) : List.replicate n a \u2286 [a]"}, {"doc": null, "module": "Mathlib.Data.List.Basic", "name": "List.replicate_left_inj", "type": " {\u03b1 : Type u} {a : \u03b1} {n m : \u2115} : List.replicate n a = List.replicate m a \u2194 n = m"}, {"doc": null, "module": "Mathlib.Data.List.Basic", "name": "List.replicate_right_inj", "type": " {\u03b1 : Type u} {a b : \u03b1} {n : \u2115} (hn : n \u2260 0) : List.replicate n a = List.replicate n b \u2194 a = b"}, {"doc": null, "module": "Mathlib.Data.List.Basic", "name": "List.replicate_right_inj'", "type": " {\u03b1 : Type u} {a b : \u03b1} {n : \u2115} : List.replicate n a = List.replicate n b \u2194 n = 0 \u2228 a = b"}, {"doc": null, "module": "Mathlib.Data.List.Basic", "name": "List.replicate_add", "type": " {\u03b1 : Type u} (m n : \u2115) (a : \u03b1) : List.replicate (m + n) a = List.replicate m a ++ List.replicate n a"}, {"doc": null, "module": "Mathlib.Data.List.Dedup", "name": "List.replicate_dedup", "type": " {\u03b1 : Type u_1} [DecidableEq \u03b1] {x : \u03b1} {k : \u2115} : k \u2260 0 \u2192 (List.replicate k x).dedup = [x]"}]}