mathlib3 documentation

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} :
has_mem α (list α)
Equations
@[protected, instance]
def list.decidable_mem {α : Type u} [decidable_eq α] (a : α) (l : list α) :
Equations
@[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
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
@[simp]
def list.join {α : Type u} :
list (list α) list α
Equations
def list.filter_map {α : Type u} {β : Type v} (f : α 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.

after      (eq 1)       [0, 1, 2, 3] = [2, 3]
drop_while (not  eq 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] :
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
@[simp]
def list.take {α : Type u} :
Equations
@[simp]
def list.foldl {α : Type u} {β : Type v} (f : α β α) :
α list β α
Equations
@[simp]
def list.foldr {α : Type u} {β : Type v} (f : α β β) (b : β) :
list α β
Equations
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 α] :
Equations
@[protected, instance]
def list.has_singleton {α : Type u} :
Equations
@[protected, instance]
@[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
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 α] [h : decidable_rel has_lt.lt] (l₁ l₂ : list α) :
decidable (l₁ < l₂)
Equations
@[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 α] [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 α] :

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