# mathlibdocumentation

core.init.data.list.basic

@[instance]
def list.inhabited (α : Type u) :

Equations
def list.has_dec_eq {α : Type u} [s : decidable_eq α] :

Equations
• list.has_dec_eq (a :: as) (b :: bs) = list.has_dec_eq._match_1 a as b bs (λ (hab : a = b), bs) (s a b)
• list.has_dec_eq (a :: as) list.nil =
• (b :: bs) =
• = is_true list.has_dec_eq._main._proof_1
• list.has_dec_eq._match_1 a as b bs _f_1 (is_true hab) = list.has_dec_eq._match_2 a as b bs hab (_f_1 hab)
• list.has_dec_eq._match_1 a as b bs _f_1 (is_false nab) =
• list.has_dec_eq._match_2 a as b bs hab (is_true habs) =
• list.has_dec_eq._match_2 a as b bs hab (is_false nabs) =
@[instance]
def list.decidable_eq {α : Type u} [decidable_eq α] :

Equations
@[simp]
def list.append {α : Type u} :
list αlist αlist α

Equations
@[instance]
def list.has_append {α : Type u} :

Equations
def list.mem {α : Type u} :
α → list α → Prop

Equations
@[instance]
def list.has_mem {α : Type u} :
(list α)

Equations
@[instance]
def list.decidable_mem {α : Type u} [decidable_eq α] (a : α) (l : list α) :

Equations
• (b :: l) = dite (a = b) (λ (h₁ : a = b), is_true _) (λ (h₁ : ¬a = b), list.decidable_mem._match_1 a b l h₁ l))
• list.decidable_mem._match_1 a b l h₁ (is_true h₂) =
• list.decidable_mem._match_1 a b l h₁ (is_false h₂) =
@[instance]
def list.has_emptyc {α : Type u} :

Equations
def list.erase {α : Type u_1} [decidable_eq α] :
list αα → list α

Equations
def list.bag_inter {α : Type u_1} [decidable_eq α] :
list αlist αlist α

Equations
def list.diff {α : Type u_1} [decidable_eq α] :
list αlist αlist α

Equations
@[simp]
def list.length {α : Type u} :
list α

Equations
def list.empty {α : Type u} :
list αbool

Equations
@[simp]
def list.nth {α : Type u} :
list α

Equations
@[simp]
def list.nth_le {α : Type u} (l : list α) (n : ) :
n < l.length → α

Equations
@[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} :
(α → β)list αlist β

Equations
@[simp]
def list.map₂ {α : Type u} {β : Type v} {γ : Type w} :
(α → β → γ)list αlist βlist γ

Equations
def list.map_with_index_core {α : Type u} {β : Type v} :
(α → β)list αlist β

Equations
• (a :: as) = f k a :: (k + 1) as
def list.map_with_index {α : Type u} {β : Type v} :
(α → β)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} :
(α → option β)list αlist β

Equations
• (a :: l) = list.filter_map._match_1 l) l) (f a)
• list.filter_map._match_1 _f_1 _f_2 (some b) = b :: _f_2
• list.filter_map._match_1 _f_1 _f_2 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.

lean 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)  :
list α

Equations
def list.index_of {α : Type u} [decidable_eq α] :
α → list α

Equations
def list.remove_all {α : Type u} [decidable_eq α] :
list αlist αlist α

Equations
def list.update_nth {α : Type u} :
list αα → list α

Equations
def list.remove_nth {α : Type u} :
list αlist α

Equations
@[simp]
def list.drop {α : Type u} :
list αlist α

Equations
• (x :: r) = r
• a = a
@[simp]
def list.take {α : Type u} :
list αlist α

Equations
@[simp]
def list.foldl {α : Type u} {β : Type v} :
(α → β → α)α → list β → α

Equations
• a (b :: l) = (f a b) l
• = a
@[simp]
def list.foldr {α : Type u} {β : Type v} :
(α → β → β)β → list α → β

Equations
• b (a :: l) = f a b l)
• = b
def list.any {α : Type u} :
list α(α → bool)bool

Equations
def list.all {α : Type u} :
list α(α → bool)bool

Equations
def list.bor  :

Equations
def list.band  :

Equations
def list.zip_with {α : Type u} {β : Type v} {γ : Type w} :
(α → β → γ)list αlist βlist γ

Equations
def list.zip {α : Type u} {β : Type v} :
list αlist βlist × β)

Equations
def list.unzip {α : Type u} {β : Type v} :
list × β)list α × list β

Equations
def list.insert {α : Type u} [decidable_eq α] :
α → list αlist α

Equations
@[instance]
def list.has_insert {α : Type u} [decidable_eq α] :
(list α)

Equations
@[instance]
def list.has_singleton {α : Type u} :
(list α)

Equations
@[instance]
def list.is_lawful_singleton {α : Type u} [decidable_eq α] :
(list α)

Equations
def list.union {α : Type u} [decidable_eq α] :
list αlist αlist α

Equations
@[instance]
def list.has_union {α : Type u} [decidable_eq α] :

Equations
def list.inter {α : Type u} [decidable_eq α] :
list αlist αlist α

Equations
@[instance]
def list.has_inter {α : Type u} [decidable_eq α] :

Equations
@[simp]
def list.repeat {α : Type u} :
α → list α

Equations
def list.range_core  :

Equations
def list.range  :

Equations
def list.iota  :

Equations
def list.enum_from {α : Type u} :
list αlist ( × α)

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} :
α → list αlist α

Equations
def list.intercalate {α : Type u} :
list αlist (list α)list α

Equations
def list.bind {α : Type u} {β : Type v} :
list α(α → list β)list β

Equations
def list.ret {α : Type u} :
α → list α

Equations
• = [a]
def list.lt {α : Type u} [has_lt α] :
list αlist α → Prop

Equations
@[instance]
def list.has_lt {α : Type u} [has_lt α] :

Equations
@[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 (is_true h₁) =
• list.has_decidable_lt._match_1 a as b bs _f_1 (is_false h₁) = 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 (is_true h₂) =
• list.has_decidable_lt._match_2 a as b bs h₁ _f_1 (is_false h₂) = 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₂ (is_true h₃) =
• list.has_decidable_lt._match_4 a as b bs h₁ h₂ (is_false h₃) =
def list.le {α : Type u} [has_lt α] :
list αlist α → Prop

Equations
@[instance]
def list.has_le {α : Type u} [has_lt α] :

Equations
@[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 αlist αbool

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

Equations
def list.is_suffix_of {α : Type u} [decidable_eq α] :
list αlist αbool

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

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

Equations