core / init.data.list.basic

source

@[protected, instance]

def list.inhabited (α : Type u) :

inhabited (list α)

Equations

list.inhabited α = {default := list.nil α}

source

@[protected]

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

decidable_eq (list α)

Equations

list.has_dec_eq (a :: as) (b :: bs) = list.has_dec_eq._match_1 a as b bs (λ (hab : a = b), list.has_dec_eq as bs) (s a b)
list.has_dec_eq (a :: as) list.nil = is_false _
list.has_dec_eq list.nil (b :: bs) = is_false _
list.has_dec_eq list.nil list.nil = 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) = is_false _
list.has_dec_eq._match_2 a as b bs hab (is_true habs) = is_true _
list.has_dec_eq._match_2 a as b bs hab (is_false nabs) = is_false _

source

@[protected, instance]

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

decidable_eq (list α)

Equations

list.decidable_eq = list.has_dec_eq

source

@[protected, simp]

def list.append {α : Type u} :

list α → list α → list α

Equations

(h :: s).append t = h :: s.append t
list.nil.append l = l

source

@[protected, instance]

def list.has_append {α : Type u} :

has_append (list α)

Equations

list.has_append = {append := list.append α}

source

@[protected]

def list.mem {α : Type u} :

α → list α → Prop

Equations

list.mem a (b :: l) = (a = b ∨ list.mem a l)
list.mem a list.nil = false

source

@[protected, instance]

def list.has_mem {α : Type u} :

has_mem α (list α)

Equations

list.has_mem = {mem := list.mem α}

source

@[protected, instance]

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

decidable (a ∈ l)

Equations

list.decidable_mem a (b :: l) = dite (a = b) (λ (h₁ : a = b), is_true _) (λ (h₁ : ¬a = b), list.decidable_mem._match_1 a b l h₁ (list.decidable_mem a l))
list.decidable_mem a list.nil = is_false not_false
list.decidable_mem._match_1 a b l h₁ (is_true h₂) = is_true _
list.decidable_mem._match_1 a b l h₁ (is_false h₂) = is_false _

source

@[protected, instance]

def list.has_emptyc {α : Type u} :

has_emptyc (list α)

Equations

list.has_emptyc = {emptyc := list.nil α}

source

@[protected]

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

list α → α → list α

Equations

(a :: l).erase b = ite (a = b) l (a :: l.erase b)
list.nil.erase b = list.nil

source

@[protected]

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

list α → list α → list α

Equations

(a :: l₁).bag_inter (hd :: tl) = ite (a ∈ hd :: tl) (a :: l₁.bag_inter ((hd :: tl).erase a)) (l₁.bag_inter (hd :: tl))
(hd :: tl).bag_inter list.nil = list.nil
list.nil.bag_inter (hd :: tl) = list.nil
list.nil.bag_inter list.nil = list.nil

source

@[protected]

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

list α → list α → list α

Equations

l₁.diff (a :: l₂) = ite (a ∈ l₁) ((l₁.erase a).diff l₂) (l₁.diff l₂)
l.diff list.nil = l

source

@[simp]

def list.length {α : Type u} :

list α → ℕ

Equations

(a :: l).length = l.length + 1
list.nil.length = 0

source

@[simp]

def list.empty {α : Type u} :

list α → bool

Equations

(_x :: _x_1).empty = ff
list.nil.empty = tt

source

@[simp]

def list.nth {α : Type u} :

list α → ℕ → option α

Equations

(a :: l).nth (n + 1) = l.nth n
(a :: l).nth 0 = some a
list.nil.nth n = none

source

@[simp]

def list.nth_le {α : Type u} (l : list α) (n : ℕ) :

n < l.length → α

Equations

(a :: l).nth_le (n + 1) h = l.nth_le n _
(a :: l).nth_le 0 h = a
list.nil.nth_le n h = absurd h _

source

@[simp]

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

list α → α

Equations

(a :: l).head = a
list.nil.head = default

source

@[simp]

def list.tail {α : Type u} :

list α → list α

Equations

(a :: l).tail = l
list.nil.tail = list.nil

source

def list.reverse_core {α : Type u} :

list α → list α → list α

Equations

(a :: l).reverse_core r = l.reverse_core (a :: r)
list.nil.reverse_core r = r

source

def list.reverse {α : Type u} :

list α → list α

Equations

list.reverse = λ (l : list α), l.reverse_core list.nil

source

@[simp]

def list.map {α : Type u} {β : Type v} (f : α → β) :

list α → list β

Equations

list.map f (a :: l) = f a :: list.map f l
list.map f list.nil = list.nil

source

@[simp]

def list.map₂ {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) :

list α → list β → list γ

Equations

list.map₂ f (x :: xs) (y :: ys) = f x y :: list.map₂ f xs ys
list.map₂ f (hd :: tl) list.nil = list.nil
list.map₂ f list.nil (hd :: tl) = list.nil
list.map₂ f list.nil list.nil = list.nil

source

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

ℕ → list α → list β

Equations

list.map_with_index_core f k (a :: as) = f k a :: list.map_with_index_core f (k + 1) as
list.map_with_index_core f k list.nil = list.nil

source

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

list.map_with_index f as = list.map_with_index_core f 0 as

source

@[simp]

def list.join {α : Type u} :

list (list α) → list α

Equations

(l :: ls).join = l ++ ls.join
list.nil.join = list.nil

source

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

list α → list β

Equations

list.filter_map f (a :: l) = list.filter_map._match_1 (list.filter_map f l) (list.filter_map f l) (f a)
list.filter_map f list.nil = list.nil
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

source

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

list α → list α

Equations

list.filter p (a :: l) = ite (p a) (a :: list.filter p l) (list.filter p l)
list.filter p list.nil = list.nil

source

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

list α → list α × list α

Equations

list.partition p (a :: l) = list.partition._match_1 p a (list.partition p l)
list.partition p list.nil = (list.nil α, list.nil α)
list.partition._match_1 p a (l₁, l₂) = ite (p a) (a :: l₁, l₂) (l₁, a :: l₂)

source

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

list α → list α

Equations

list.drop_while p (a :: l) = ite (p a) (list.drop_while p l) (a :: l)
list.drop_while p list.nil = list.nil

source

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

list.after p (x :: xs) = ite (p x) xs (list.after p xs)
list.after p list.nil = list.nil

source

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

list α → list α × list α

Equations

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 α] (a : α) :

list α → ℕ

Equations

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

source

def list.remove_all {α : Type u} [decidable_eq α] (xs ys : 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} (f : α → β → α) :

α → 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} (f : α → β → β) (b : β) :

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} (l : list α) (p : α → bool) :

bool

Equations

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

source

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

bool

Equations

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

source

def list.bor (l : list bool) :

bool

Equations

l.bor = l.any id

source

def list.band (l : list bool) :

bool

Equations

l.band = l.all id

source

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

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

@[protected]

def list.insert {α : Type u} [decidable_eq α] (a : α) (l : list α) :

list α

Equations

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

source

@[protected, 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

@[protected, instance]

def list.has_singleton {α : Type u} :

has_singleton α (list α)

Equations

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

source

@[protected, instance]

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

is_lawful_singleton α (list α)

source

@[protected]

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

list α

Equations

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

source

@[protected, 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

@[protected]

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

list α

Equations

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

source

@[protected, 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} (a : α) :

ℕ → 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 (n : ℕ) :

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} (sep : α) :

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} (sep : list α) (xs : list (list α)) :

list α

Equations

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

source

@[protected]

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

list β

Equations

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

source

@[protected]

def list.ret {α : Type u} (a : α) :

list α

Equations

list.ret a = [a]

source

@[protected]

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

@[protected, instance]

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

has_lt (list α)

Equations

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

source

@[protected, 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 = is_false not_false
list.nil.has_decidable_lt (b :: bs) = is_true trivial
list.nil.has_decidable_lt list.nil = is_false not_false
list.has_decidable_lt._match_1 a as b bs _f_1 (is_true h₁) = is_true _
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₂) = is_false _
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₃) = is_true _
list.has_decidable_lt._match_4 a as b bs h₁ h₂ (is_false h₃) = is_false _