mathlib documentation

data.list.indexes

Lemmas about list.*_with_index functions. #

Some specification lemmas for list.map_with_index, list.mmap_with_index, list.foldl_with_index and list.foldr_with_index.

@[simp]
theorem list.map_with_index_nil {α : Type u_1} {β : Type u_2} (f : α → β) :
theorem list.map_with_index_core_eq {α : Type u} {β : Type v} (l : list α) (f : α → β) (n : ) :
list.map_with_index_core f n l = list.map_with_index (λ (i : ) (a : α), f (i + n) a) l
theorem list.map_with_index_eq_enum_map {α : Type u} {β : Type v} (l : list α) (f : α → β) :
@[simp]
theorem list.map_with_index_cons {α : Type u_1} {β : Type u_2} (l : list α) (f : α → β) (a : α) :
list.map_with_index f (a :: l) = f 0 a :: list.map_with_index (λ (i : ), f (i + 1)) l
@[simp]
theorem list.length_map_with_index {α : Type u_1} {β : Type u_2} (l : list α) (f : α → β) :
@[simp]
theorem list.nth_le_map_with_index {α : Type u_1} {β : Type u_2} (l : list α) (f : α → β) (i : ) (h : i < l.length) (h' : i < (list.map_with_index f l).length := _) :
(list.map_with_index f l).nth_le i h' = f i (l.nth_le i h)
theorem list.map_with_index_eq_of_fn {α : Type u_1} {β : Type u_2} (l : list α) (f : α → β) :
list.map_with_index f l = list.of_fn (λ (i : fin l.length), f i (l.nth_le i _))
def list.foldr_with_index_aux_spec {α : Type u} {β : Type v} (f : α → β → β) (start : ) (b : β) (as : list α) :
β

Specification of foldr_with_index_aux.

Equations
theorem list.foldr_with_index_aux_spec_cons {α : Type u} {β : Type v} (f : α → β → β) (start : ) (b : β) (a : α) (as : list α) :
list.foldr_with_index_aux_spec f start b (a :: as) = f start a (list.foldr_with_index_aux_spec f (start + 1) b as)
theorem list.foldr_with_index_aux_eq_foldr_with_index_aux_spec {α : Type u} {β : Type v} (f : α → β → β) (start : ) (b : β) (as : list α) :
theorem list.foldr_with_index_eq_foldr_enum {α : Type u} {β : Type v} (f : α → β → β) (b : β) (as : list α) :
theorem list.indexes_values_eq_filter_enum {α : Type u} (p : α → Prop) [decidable_pred p] (as : list α) :
theorem list.find_indexes_eq_map_indexes_values {α : Type u} (p : α → Prop) [decidable_pred p] (as : list α) :
def list.foldl_with_index_aux_spec {α : Type u} {β : Type v} (f : α → β → α) (start : ) (a : α) (bs : list β) :
α

Specification of foldl_with_index_aux.

Equations
theorem list.foldl_with_index_aux_spec_cons {α : Type u} {β : Type v} (f : α → β → α) (start : ) (a : α) (b : β) (bs : list β) :
list.foldl_with_index_aux_spec f start a (b :: bs) = list.foldl_with_index_aux_spec f (start + 1) (f start a b) bs
theorem list.foldl_with_index_aux_eq_foldl_with_index_aux_spec {α : Type u} {β : Type v} (f : α → β → α) (start : ) (a : α) (bs : list β) :
theorem list.foldl_with_index_eq_foldl_enum {α : Type u} {β : Type v} (f : α → β → α) (a : α) (bs : list β) :
list.foldl_with_index f a bs = list.foldl (λ (a : α) (p : × β), f p.fst a p.snd) a bs.enum
theorem list.mfoldr_with_index_eq_mfoldr_enum {m : Type uType v} [monad m] {α : Type u_1} {β : Type u} (f : α → β → m β) (b : β) (as : list α) :
theorem list.mfoldl_with_index_eq_mfoldl_enum {m : Type uType v} [monad m] [is_lawful_monad m] {α : Type u_1} {β : Type u} (f : β → α → m β) (b : β) (as : list α) :
list.mfoldl_with_index f b as = list.mfoldl (λ (b : β) (p : × α), f p.fst b p.snd) b as.enum
def list.mmap_with_index_aux_spec {m : Type uType v} [applicative m] {α : Type u_1} {β : Type u} (f : α → m β) (start : ) (as : list α) :
m (list β)

Specification of mmap_with_index_aux.

Equations
theorem list.mmap_with_index_aux_spec_cons {m : Type uType v} [applicative m] {α : Type u_1} {β : Type u} (f : α → m β) (start : ) (a : α) (as : list α) :
theorem list.mmap_with_index_aux_eq_mmap_with_index_aux_spec {m : Type uType v} [applicative m] {α : Type u_1} {β : Type u} (f : α → m β) (start : ) (as : list α) :
theorem list.mmap_with_index_eq_mmap_enum {m : Type uType v} [applicative m] {α : Type u_1} {β : Type u} (f : α → m β) (as : list α) :
theorem list.mmap_with_index'_aux_eq_mmap_with_index_aux {m : Type uType v} [applicative m] [is_lawful_applicative m] {α : Type u_1} (f : α → m punit) (start : ) (as : list α) :
theorem list.mmap_with_index'_eq_mmap_with_index {m : Type uType v} [applicative m] [is_lawful_applicative m] {α : Type u_1} (f : α → m punit) (as : list α) :