mathlib documentation

core.init.data.list.basic

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

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

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

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

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

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
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
@[simp]
def list.join {α : Type u} :
list (list α)list α

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

Equations
def list.filter {α : Type u} (p : α → Prop) [decidable_pred p] :
list αlist α

Equations
def list.partition {α : Type u} (p : α → Prop) [decidable_pred p] :
list αlist α × list α

Equations
def list.drop_while {α : Type u} (p : α → Prop) [decidable_pred p] :
list αlist α

Equations
def list.after {α : Type u} (p : α → Prop) [decidable_pred p] :
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 (noteq 1) [0, 1, 2, 3] = [1, 2, 3]

Equations
def list.span {α : Type u} (p : α → Prop) [decidable_pred p] :
list αlist α × list α

Equations
def list.find_index {α : Type u} (p : α → Prop) [decidable_pred p] :
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
@[simp]
def list.take {α : Type u} :
list αlist α

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

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

Equations
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 α] :

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

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.enum_from {α : Type u} :
list αlist ( × α)

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

Equations
@[simp]
def list.last {α : Type u} (l : list α) :
l list.nil → α

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
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 α] [h : decidable_rel has_lt.lt] (l₁ l₂ : list α) :
decidable (l₁ < l₂)

Equations
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 α] [h : decidable_rel has_lt.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 α] [decidable_rel has_lt.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} :
bin_tree αlist α

Equations