mathlib docs: core.init.data.list.basic

list.span p (a :: xs) = ite (p a) (list.span._match_1 a (list.span p xs)) (list.nil α, a :: xs)
list.span p list.nil = (list.nil α, list.nil α)
list.span._match_1 a (l, r) = (a :: l, r)

source

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

list α → ℕ

Equations

list.find_index p (a :: l) = ite (p a) 0 (list.find_index p l).succ
list.find_index p list.nil = 0

source

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

α → list α → ℕ

Equations

list.index_of a = list.find_index (eq a)

source

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

list α → list α → list α

Equations

xs.remove_all ys = list.filter (λ (_x : α), _x ∉ ys) xs

source

def list.update_nth {α : Type u} :

list α → ℕ → α → list α

Equations

(x :: xs).update_nth (i + 1) a = x :: xs.update_nth i a
(x :: xs).update_nth 0 a = a :: xs
list.nil.update_nth _x _x_1 = list.nil

source

def list.remove_nth {α : Type u} :

list α → ℕ → list α

Equations

(x :: xs).remove_nth (i + 1) = x :: xs.remove_nth i
(x :: xs).remove_nth 0 = xs
list.nil.remove_nth _x = list.nil

source

@[simp]

def list.drop {α : Type u} :

ℕ → list α → list α

Equations

list.drop n.succ (x :: r) = list.drop n r
list.drop n.succ list.nil = list.nil
list.drop 0 a = a

source

@[simp]

def list.take {α : Type u} :

ℕ → list α → list α

Equations

list.take n.succ (x :: r) = x :: list.take n r
list.take n.succ list.nil = list.nil
list.take 0 a = list.nil

source

@[simp]

def list.foldl {α : Type u} {β : Type v} :

(α → β → α) → α → list β → α

Equations

list.foldl f a (b :: l) = list.foldl f (f a b) l
list.foldl f a list.nil = a

source

@[simp]

def list.foldr {α : Type u} {β : Type v} :

(α → β → β) → β → list α → β

Equations

list.foldr f b (a :: l) = f a (list.foldr f b l)
list.foldr f b list.nil = b

source

def list.any {α : Type u} :

list α → (α → bool) → bool

Equations

l.any p = list.foldr (λ (a : α) (r : bool), p a || r) bool.ff l

source

def list.all {α : Type u} :

list α → (α → bool) → bool

Equations

l.all p = list.foldr (λ (a : α) (r : bool), p a && r) bool.tt l

source

def list.bor :

list bool → bool

Equations

l.bor = l.any id

source

def list.band :

list bool → bool

Equations

l.band = l.all id

source

def list.zip_with {α : Type u} {β : Type v} {γ : Type w} :

(α → β → γ) → list α → list β → list γ

Equations

list.zip_with f (x :: xs) (y :: ys) = f x y :: list.zip_with f xs ys
list.zip_with f (hd :: tl) list.nil = list.nil
list.zip_with f list.nil _x = list.nil

source

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

list α → list β → list (α × β)

Equations

list.zip = list.zip_with prod.mk

source

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

list (α × β) → list α × list β

Equations

((a, b) :: t).unzip = list.unzip._match_1 a b t.unzip
list.nil.unzip = (list.nil α, list.nil β)
list.unzip._match_1 a b (al, bl) = (a :: al, b :: bl)

source

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

α → list α → list α

Equations

list.insert a l = ite (a ∈ l) l (a :: l)

source

@[instance]

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

has_insert α (list α)

Equations

list.has_insert = {insert := list.insert (λ (a b : α), _inst_1 a b)}

source

@[instance]

def list.has_singleton {α : Type u} :

has_singleton α (list α)

Equations

list.has_singleton = {singleton := λ (x : α), [x]}

source

@[instance]

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

is_lawful_singleton α (list α)

Equations

list.is_lawful_singleton = {insert_emptyc_eq := _}

source

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

list α → list α → list α

Equations

l₁.union l₂ = list.foldr has_insert.insert l₂ l₁

source

@[instance]

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

has_union (list α)

Equations

list.has_union = {union := list.union (λ (a b : α), _inst_1 a b)}

source

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

list α → list α → list α

Equations

l₁.inter l₂ = list.filter (λ (_x : α), _x ∈ l₂) l₁

source

@[instance]

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

has_inter (list α)

Equations

list.has_inter = {inter := list.inter (λ (a b : α), _inst_1 a b)}

source

@[simp]

def list.repeat {α : Type u} :

α → ℕ → list α

Equations

list.repeat a n.succ = a :: list.repeat a n
list.repeat a 0 = list.nil

source

def list.range_core :

ℕ → list ℕ → list ℕ

Equations

list.range_core n.succ l = list.range_core n (n :: l)
list.range_core 0 l = l

source

def list.range :

ℕ → list ℕ

Equations

list.range n = list.range_core n list.nil

source

def list.iota :

ℕ → list ℕ

Equations

list.iota n.succ = n.succ :: list.iota n
list.iota 0 = list.nil

source

def list.enum_from {α : Type u} :

ℕ → list α → list (ℕ × α)

Equations

list.enum_from n (x :: xs) = (n, x) :: list.enum_from (n + 1) xs
list.enum_from n list.nil = list.nil

source

def list.enum {α : Type u} :

list α → list (ℕ × α)

Equations

list.enum = list.enum_from 0

source

@[simp]

def list.last {α : Type u} (l : list α) :

l ≠ list.nil → α

Equations

(a :: b :: l).last h = (b :: l).last _
[a].last h = a
list.nil.last h = absurd list.last._main._proof_1 h

source

def list.ilast {α : Type u} [inhabited α] :

list α → α

Equations

(a :: b :: hd :: tl).ilast = (hd :: tl).ilast
[a, b].ilast = b
[a].ilast = a
list.nil.ilast = arbitrary α

source

def list.init {α : Type u} :

list α → list α

Equations

(a :: hd :: tl).init = a :: (hd :: tl).init
[a].init = list.nil
list.nil.init = list.nil

source

def list.intersperse {α : Type u} :

α → list α → list α

Equations

list.intersperse sep (x :: hd :: tl) = x :: sep :: list.intersperse sep (hd :: tl)
list.intersperse sep [x] = [x]
list.intersperse sep list.nil = list.nil

source

def list.intercalate {α : Type u} :

list α → list (list α) → list α

Equations

sep.intercalate xs = (list.intersperse sep xs).join

source

def list.bind {α : Type u} {β : Type v} :

list α → (α → list β) → list β

Equations

a.bind b = (list.map b a).join

source

def list.ret {α : Type u} :

α → list α

Equations

list.ret a = [a]

source

def list.lt {α : Type u} [has_lt α] :

list α → list α → Prop

Equations

(a :: as).lt (b :: bs) = (a < b ∨ ¬b < a ∧ as.lt bs)
(a :: as).lt list.nil = false
list.nil.lt (b :: bs) = true
list.nil.lt list.nil = false

source

@[instance]

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

has_lt (list α)

Equations

list.has_lt = {lt := list.lt _inst_1}

source

@[instance]

def list.has_decidable_lt {α : Type u} [has_lt α] [h : decidable_rel has_lt.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)
(a :: as).has_decidable_lt list.nil = decidable.is_false not_false
list.nil.has_decidable_lt (b :: bs) = decidable.is_true trivial
list.nil.has_decidable_lt list.nil = decidable.is_false not_false
list.has_decidable_lt._match_1 a as b bs _f_1 (decidable.is_true h₁) = decidable.is_true _
list.has_decidable_lt._match_1 a as b bs _f_1 (decidable.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 (decidable.is_true h₂) = decidable.is_false _
list.has_decidable_lt._match_2 a as b bs h₁ _f_1 (decidable.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₂ (decidable.is_true h₃) = decidable.is_true _
list.has_decidable_lt._match_4 a as b bs h₁ h₂ (decidable.is_false h₃) = decidable.is_false _