# mathlib3documentation

core / init.data.list.basic

@[protected, instance]
def list.inhabited (α : Type u) :
Equations
@[protected]
def list.has_dec_eq {α : Type u} [s : decidable_eq α] :
Equations
@[protected, instance]
Equations
@[protected, simp]
def list.append {α : Type u} :
list α list α list α
Equations
@[protected, instance]
def list.has_append {α : Type u} :
Equations
@[protected]
def list.mem {α : Type u} :
α list α Prop
Equations
@[protected, instance]
def list.has_mem {α : Type u} :
(list α)
Equations
@[protected, instance]
def list.decidable_mem {α : Type u} [decidable_eq α] (a : α) (l : list α) :
Equations
• (b :: l) = dite (a = b) (λ (h₁ : a = b), (λ (h₁ : ¬a = b), list.decidable_mem._match_1 a b l h₁ l))
• list.decidable_mem._match_1 a b l h₁ =
• list.decidable_mem._match_1 a b l h₁ =
@[protected, instance]
def list.has_emptyc {α : Type u} :
Equations
@[protected]
def list.erase {α : Type u_1} [decidable_eq α] :
list α α list α
Equations
@[protected]
def list.bag_inter {α : Type u_1} [decidable_eq α] :
list α list α list α
Equations
@[protected]
def list.diff {α : Type u_1} [decidable_eq α] :
list α list α list α
Equations
@[simp]
def list.length {α : Type u} :
Equations
@[simp]
def list.empty {α : Type u} :
Equations
@[simp]
def list.nth {α : Type u} :
Equations
@[simp]
def list.nth_le {α : Type u} (l : list α) (n : ) :
n < l.length α
Equations
Instances for list.nth_le
@[simp]
def list.head {α : Type u} [inhabited α] :
list α α
Equations
@[simp]
def list.tail {α : Type u} :
list α list α
Equations
def list.reverse_core {α : Type u} :
list α list α list α
Equations
def list.reverse {α : Type u} :
list α list α
Equations
@[simp]
def list.map {α : Type u} {β : Type v} (f : α β) :
list α list β
Equations
Instances for list.map
@[simp]
def list.map₂ {α : Type u} {β : Type v} {γ : Type w} (f : α β γ) :
list α list β list γ
Equations
def list.map_with_index_core {α : Type u} {β : Type v} (f : α β) :
Equations
• (a :: as) = f k a :: (k + 1) as
def list.map_with_index {α : Type u} {β : Type v} (f : α β) (as : list α) :
list β

Given a function f : ℕ → α → β and as : list α, as = [a₀, a₁, ...], returns the list [f 0 a₀, f 1 a₁, ...].

Equations
• = as
@[simp]
def list.join {α : Type u} :
list (list α) list α
Equations
def list.filter_map {α : Type u} {β : Type v} (f : α ) :
list α list β
Equations
• (a :: l) = list.filter_map._match_1 l) l) (f a)
• list.filter_map._match_1 _f_1 _f_2 (option.some b) = b :: _f_2
• list.filter_map._match_1 _f_1 _f_2 option.none = _f_1
def list.filter {α : Type u} (p : α Prop)  :
list α list α
Equations
def list.partition {α : Type u} (p : α Prop)  :
list α list α × list α
Equations
• (a :: l) = list.partition._match_1 p a l)
• = (list.nil α, list.nil α)
• list.partition._match_1 p a (l₁, l₂) = ite (p a) (a :: l₁, l₂) (l₁, a :: l₂)
def list.drop_while {α : Type u} (p : α Prop)  :
list α list α
Equations
def list.after {α : Type u} (p : α Prop)  :
list α list α

after p xs is the suffix of xs after the first element that satisfies p, not including that element.

after      (eq 1)       [0, 1, 2, 3] = [2, 3]
drop_while (not ∘ eq 1) [0, 1, 2, 3] = [1, 2, 3]

Equations
• (x :: xs) = ite (p x) xs xs)
def list.span {α : Type u} (p : α Prop)  :
list α list α × list α
Equations
def list.find_index {α : Type u} (p : α Prop)  :
Equations
def list.index_of {α : Type u} [decidable_eq α] (a : α) :
Equations
def list.remove_all {α : Type u} [decidable_eq α] (xs ys : list α) :
list α
Equations
def list.update_nth {α : Type u} :
list α α list α
Equations
def list.remove_nth {α : Type u} :
Equations
@[simp]
def list.drop {α : Type u} :
Equations
• (x :: r) = r
• a = a
@[simp]
def list.take {α : Type u} :
Equations
@[simp]
def list.foldl {α : Type u} {β : Type v} (f : α β α) :
α list β α
Equations
• a (b :: l) = (f a b) l
• = a
@[simp]
def list.foldr {α : Type u} {β : Type v} (f : α β β) (b : β) :
list α β
Equations
• b (a :: l) = f a b l)
• = b
def list.any {α : Type u} (l : list α) (p : α bool) :
Equations
def list.all {α : Type u} (l : list α) (p : α bool) :
Equations
def list.bor (l : list bool) :
Equations
def list.band (l : list bool) :
Equations
def list.zip_with {α : Type u} {β : Type v} {γ : Type w} (f : α β γ) :
list α list β list γ
Equations
Instances for list.zip_with
def list.zip {α : Type u} {β : Type v} :
list α list β list × β)
Equations
def list.unzip {α : Type u} {β : Type v} :
list × β) list α × list β
Equations
@[protected]
def list.insert {α : Type u} [decidable_eq α] (a : α) (l : list α) :
list α
Equations
@[protected, instance]
def list.has_insert {α : Type u} [decidable_eq α] :
(list α)
Equations
@[protected, instance]
def list.has_singleton {α : Type u} :
(list α)
Equations
@[protected, instance]
def list.is_lawful_singleton {α : Type u} [decidable_eq α] :
(list α)
@[protected]
def list.union {α : Type u} [decidable_eq α] (l₁ l₂ : list α) :
list α
Equations
@[protected, instance]
def list.has_union {α : Type u} [decidable_eq α] :
Equations
@[protected]
def list.inter {α : Type u} [decidable_eq α] (l₁ l₂ : list α) :
list α
Equations
@[protected, instance]
def list.has_inter {α : Type u} [decidable_eq α] :
Equations
@[simp]
def list.repeat {α : Type u} (a : α) :
Equations
Equations
def list.range (n : ) :
Equations
def list.iota  :
Equations
def list.enum_from {α : Type u} :
Equations
def list.enum {α : Type u} :
list α list ( × α)
Equations
@[simp]
def list.last {α : Type u} (l : list α) :
α
Equations
def list.ilast {α : Type u} [inhabited α] :
list α α
Equations
def list.init {α : Type u} :
list α list α
Equations
def list.intersperse {α : Type u} (sep : α) :
list α list α
Equations
def list.intercalate {α : Type u} (sep : list α) (xs : list (list α)) :
list α
Equations
@[protected]
def list.bind {α : Type u} {β : Type v} (a : list α) (b : α list β) :
list β
Equations
@[protected]
def list.ret {α : Type u} (a : α) :
list α
Equations
@[protected]
def list.lt {α : Type u} [has_lt α] :
list α list α Prop
Equations
@[protected, instance]
def list.has_lt {α : Type u} [has_lt α] :
Equations
@[protected, instance]
def list.has_decidable_lt {α : Type u} [has_lt α] (l₁ l₂ : list α) :
decidable (l₁ < l₂)
Equations
• (a :: as).has_decidable_lt (b :: bs) = list.has_decidable_lt._match_1 a as b bs (λ (h₁ : ¬a < b) (h₂ : ¬b < a), as.has_decidable_lt bs) (h a b)
• list.has_decidable_lt._match_1 a as b bs _f_1 =
• list.has_decidable_lt._match_1 a as b bs _f_1 = list.has_decidable_lt._match_2 a as b bs h₁ (λ (h₂ : ¬b < a), _f_1 h₁ h₂) (h b a)
• list.has_decidable_lt._match_2 a as b bs h₁ _f_1 =
• list.has_decidable_lt._match_2 a as b bs h₁ _f_1 = list.has_decidable_lt._match_4 a as b bs h₁ h₂ (_f_1 h₂)
• list.has_decidable_lt._match_4 a as b bs h₁ h₂ =
• list.has_decidable_lt._match_4 a as b bs h₁ h₂ =
@[protected, reducible]
def list.le {α : Type u} [has_lt α] (a b : list α) :
Prop
Equations
@[protected, instance]
def list.has_le {α : Type u} [has_lt α] :
Equations
@[protected, instance]
def list.has_decidable_le {α : Type u} [has_lt α] (l₁ l₂ : list α) :
decidable (l₁ l₂)
Equations
theorem list.le_eq_not_gt {α : Type u} [has_lt α] (l₁ l₂ : list α) :
l₁ l₂ = ¬l₂ < l₁
theorem list.lt_eq_not_ge {α : Type u} [has_lt α] (l₁ l₂ : list α) :
l₁ < l₂ = ¬l₂ l₁
def list.is_prefix_of {α : Type u} [decidable_eq α] :
list α

is_prefix_of l₁ l₂ returns tt iff l₁ is a prefix of l₂.

Equations
def list.is_suffix_of {α : Type u} [decidable_eq α] (l₁ l₂ : list α) :

is_suffix_of l₁ l₂ returns tt iff l₁ is a suffix of l₂.

Equations
def bin_tree.to_list {α : Type u} (t : bin_tree α) :
list α
Equations