data.list.defs - mathlib3 docs

source

@[protected, instance]

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

has_sdiff (list α)

Equations

list.has_sdiff = {sdiff := list.diff (λ (a b : α), _inst_1 a b)}

source

@[simp]

def list.replicate {α : Type u_1} :

ℕ → α → list α

Create a list of n copies of a. Same as function.swap list.repeat.

Equations

list.replicate n.succ a = a :: list.replicate n a
list.replicate 0 _x = list.nil

source

def list.split_at {α : Type u_1} :

ℕ → list α → list α × list α

Split a list at an index.

split_at 2 [a, b, c] = ([a, b], [c])

Equations

list.split_at n.succ (x :: xs) = list.split_at._match_1 x (list.split_at n xs)
list.split_at n.succ list.nil = (list.nil α, list.nil α)
list.split_at 0 a = (list.nil α, a)
list.split_at._match_1 x (l, r) = (x :: l, r)

source

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

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

An auxiliary function for split_on_p.

Equations

list.split_on_p_aux P (h :: t) f = ite (P h) (f list.nil :: list.split_on_p_aux P t id) (list.split_on_p_aux P t (λ (l : list α), f (h :: l)))
list.split_on_p_aux P list.nil f = [f list.nil]

source

def list.split_on_p {α : Type u} (P : α → Prop) [decidable_pred P] (l : list α) :

list (list α)

Split a list at every element satisfying a predicate.

Equations

list.split_on_p P l = list.split_on_p_aux P l id

source

def list.split_on {α : Type u} [decidable_eq α] (a : α) (as : list α) :

list (list α)

Split a list at every occurrence of an element.

[1,1,2,3,2,4,4].split_on 2 = [[1,1],[3],[4,4]]

Equations

list.split_on a as = list.split_on_p (λ (_x : α), _x = a) as

source

@[simp]

def list.concat {α : Type u_1} :

list α → α → list α

Concatenate an element at the end of a list.

concat [a, b] c = [a, b, c]

Equations

(b :: l).concat a = b :: l.concat a
list.nil.concat a = [a]

source

@[simp]

def list.head' {α : Type u_1} :

list α → option α

head' xs returns the first element of xs if xs is non-empty; it returns none otherwise

Equations

(a :: l).head' = option.some a
list.nil.head' = option.none

source

def list.to_array {α : Type u_1} (l : list α) :

array l.length α

Convert a list into an array (whose length is the length of l).

Equations

l.to_array = {data := λ (v : fin l.length), l.nth_le v.val _}

source

def list.nthd {α : Type u_1} (l : list α) (n : ℕ) (d : α) :

α

"default" nth function: returns d instead of none in the case that the index is out of bounds.

Equations

(x :: xs).nthd (n + 1) d = xs.nthd n d
(x :: xs).nthd 0 d = x
list.nil.nthd _x d = d

source

def list.inth {α : Type u_1} [h : inhabited α] (l : list α) (n : ℕ) :

α

"inhabited" nth function: returns default instead of none in the case that the index is out of bounds.

Equations

l.inth n = l.nthd n inhabited.default

source

@[simp]

def list.modify_nth_tail {α : Type u_1} (f : list α → list α) :

ℕ → list α → list α

Apply a function to the nth tail of l. Returns the input without using f if the index is larger than the length of the list.

modify_nth_tail f 2 [a, b, c] = [a, b] ++ f [c]

Equations

list.modify_nth_tail f (n + 1) (a :: l) = a :: list.modify_nth_tail f n l
list.modify_nth_tail f (n + 1) list.nil = list.nil
list.modify_nth_tail f 0 l = f l

source

@[simp]

def list.modify_head {α : Type u_1} (f : α → α) :

list α → list α

Apply f to the head of the list, if it exists.

Equations

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

source

def list.modify_nth {α : Type u_1} (f : α → α) :

ℕ → list α → list α

Apply f to the nth element of the list, if it exists.

Equations

list.modify_nth f = list.modify_nth_tail (list.modify_head f)

source

@[simp]

def list.modify_last {α : Type u_1} (f : α → α) :

list α → list α

Apply f to the last element of l, if it exists.

Equations

list.modify_last f (x :: hd :: tl) = x :: list.modify_last f (hd :: tl)
list.modify_last f [x] = [f x]
list.modify_last f list.nil = list.nil

source

def list.insert_nth {α : Type u_1} (n : ℕ) (a : α) :

list α → list α

insert_nth n a l inserts a into the list l after the first n elements of l insert_nth 2 1 [1, 2, 3, 4] = [1, 2, 1, 3, 4]

Equations

list.insert_nth n a = list.modify_nth_tail (list.cons a) n

source

def list.take' {α : Type u_1} [inhabited α] (n : ℕ) :

list α → list α

Take n elements from a list l. If l has less than n elements, append n - length l elements default.

Equations

list.take' (n + 1) l = l.head :: list.take' n l.tail
list.take' 0 l = list.nil

source

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

list α → list α

Get the longest initial segment of the list whose members all satisfy p.

take_while (λ x, x < 3) [0, 2, 5, 1] = [0, 2]

Equations

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

source

def list.scanl {α : Type u_1} {β : Type u_2} (f : α → β → α) :

α → list β → list α

Fold a function f over the list from the left, returning the list of partial results.

scanl (+) 0 [1, 2, 3] = [0, 1, 3, 6]

Equations

list.scanl f a (b :: l) = a :: list.scanl f (f a b) l
list.scanl f a list.nil = [a]

source

def list.scanr_aux {α : Type u_1} {β : Type u_2} (f : α → β → β) (b : β) :

list α → β × list β

Auxiliary definition used to define scanr. If scanr_aux f b l = (b', l') then scanr f b l = b' :: l'

Equations

list.scanr_aux f b (a :: l) = list.scanr_aux._match_1 f a (list.scanr_aux f b l)
list.scanr_aux f b list.nil = (b, list.nil β)
list.scanr_aux._match_1 f a (b', l') = (f a b', b' :: l')

source

def list.scanr {α : Type u_1} {β : Type u_2} (f : α → β → β) (b : β) (l : list α) :

list β

Fold a function f over the list from the right, returning the list of partial results.

scanr (+) 0 [1, 2, 3] = [6, 5, 3, 0]

Equations

list.scanr f b l = list.scanr._match_1 (list.scanr_aux f b l)
list.scanr._match_1 (b', l') = b' :: l'

source

def list.prod {α : Type u_1} [has_mul α] [has_one α] :

list α → α

Product of a list.

prod [a, b, c] = ((1 * a) * b) * c

Equations

list.prod = list.foldl has_mul.mul 1

source

def list.sum {α : Type u_1} [has_add α] [has_zero α] :

list α → α

Sum of a list.

sum [a, b, c] = ((0 + a) + b) + c

Equations

list.sum = list.foldl has_add.add 0

source

def list.alternating_sum {G : Type u_1} [has_zero G] [has_add G] [has_neg G] :

list G → G

The alternating sum of a list.

Equations

(g :: h :: t).alternating_sum = g + -h + t.alternating_sum
[g].alternating_sum = g
list.nil.alternating_sum = 0

source

def list.alternating_prod {G : Type u_1} [has_one G] [has_mul G] [has_inv G] :

list G → G

The alternating product of a list.

Equations

(g :: h :: t).alternating_prod = g * h⁻¹ * t.alternating_prod
[g].alternating_prod = g
list.nil.alternating_prod = 1

source

def list.partition_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β ⊕ γ) :

list α → list β × list γ

Given a function f : α → β ⊕ γ, partition_map f l maps the list by f whilst partitioning the result it into a pair of lists, list β × list γ, partitioning the sum.inl _ into the left list, and the sum.inr _ into the right list. partition_map (id : ℕ ⊕ ℕ → ℕ ⊕ ℕ) [inl 0, inr 1, inl 2] = ([0,2], [1])

Equations

list.partition_map f (x :: xs) = list.partition_map._match_1 (list.partition_map f xs) (list.partition_map f xs) (f x)
list.partition_map f list.nil = (list.nil β, list.nil γ)
list.partition_map._match_1 _f_1 _f_2 (sum.inr r) = prod.map id (list.cons r) _f_1
list.partition_map._match_1 _f_1 _f_2 (sum.inl l) = prod.map (list.cons l) id _f_2

source

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

list α → option α

find p l is the first element of l satisfying p, or none if no such element exists.

Equations

list.find p (a :: l) = ite (p a) (option.some a) (list.find p l)
list.find p list.nil = option.none

source

def list.mfind {α : Type u} {m : Type u → Type v} [monad m] [alternative m] (tac : α → m punit) :

list α → m α

mfind tac l returns the first element of l on which tac succeeds, and fails otherwise.

Equations

list.mfind tac = list.mfirst (λ (a : α), tac a $> a)

source

def list.mbfind' {m : Type u → Type v} [monad m] {α : Type u} (p : α → m (ulift bool)) :

list α → m (option α)

mbfind' p l returns the first element a of l for which p a returns true. mbfind' short-circuits, so p is not necessarily run on every a in l. This is a monadic version of list.find.

Equations

list.mbfind' p (x :: xs) = p x >>= λ (_p : ulift bool), list.mbfind'._match_1 x (list.mbfind' p xs) _p
list.mbfind' p list.nil = has_pure.pure option.none
list.mbfind'._match_1 x _f_1 {down := px} = ite ↥px (has_pure.pure (option.some x)) _f_1

source

def list.mbfind {m : Type → Type v} [monad m] {α : Type} (p : α → m bool) (xs : list α) :

m (option α)

A variant of mbfind' with more restrictive universe levels.

Equations

list.mbfind p xs = list.mbfind' (functor.map ulift.up ∘ p) xs

source

def list.many {m : Type → Type v} [monad m] {α : Type u} (p : α → m bool) :

list α → m bool

many p as returns true iff p returns true for any element of l. many short-circuits, so if p returns true for any element of l, later elements are not checked. This is a monadic version of list.any.

Equations

list.many p (x :: xs) = p x >>= λ (px : bool), ite ↥px (has_pure.pure bool.tt) (list.many p xs)
list.many p list.nil = has_pure.pure (decidable.to_bool false)

source

def list.mall {m : Type → Type v} [monad m] {α : Type u} (p : α → m bool) (as : list α) :

m bool

mall p as returns true iff p returns true for all elements of l. mall short-circuits, so if p returns false for any element of l, later elements are not checked. This is a monadic version of list.all.

Equations

list.mall p as = bnot <$> list.many (λ (a : α), bnot <$> p a) as

source

def list.mbor {m : Type → Type v} [monad m] :

list (m bool) → m bool

mbor xs runs the actions in xs, returning true if any of them returns true. mbor short-circuits, so if an action returns true, later actions are not run. This is a monadic version of list.bor.

Equations

list.mbor = list.many id

source

def list.mband {m : Type → Type v} [monad m] :

list (m bool) → m bool

mband xs runs the actions in xs, returning true if all of them return true. mband short-circuits, so if an action returns false, later actions are not run. This is a monadic version of list.band.

Equations

list.mband = list.mall id

source

def list.foldl_with_index_aux {α : Sort u_1} {β : Type u_2} (f : ℕ → α → β → α) :

ℕ → α → list β → α

Auxiliary definition for foldl_with_index.

Equations

list.foldl_with_index_aux f i a (b :: l) = list.foldl_with_index_aux f (i + 1) (f i a b) l
list.foldl_with_index_aux f _x a list.nil = a

source

def list.foldl_with_index {α : Sort u_1} {β : Type u_2} (f : ℕ → α → β → α) (a : α) (l : list β) :

α

Fold a list from left to right as with foldl, but the combining function also receives each element's index.

Equations

list.foldl_with_index f a l = list.foldl_with_index_aux f 0 a l

source

def list.foldr_with_index_aux {α : Type u_1} {β : Sort u_2} (f : ℕ → α → β → β) :

ℕ → β → list α → β

Auxiliary definition for foldr_with_index.

Equations

list.foldr_with_index_aux f i b (a :: l) = f i a (list.foldr_with_index_aux f (i + 1) b l)
list.foldr_with_index_aux f _x b list.nil = b

source

def list.foldr_with_index {α : Type u_1} {β : Sort u_2} (f : ℕ → α → β → β) (b : β) (l : list α) :

β

Fold a list from right to left as with foldr, but the combining function also receives each element's index.

Equations

list.foldr_with_index f b l = list.foldr_with_index_aux f 0 b l

source

def list.find_indexes {α : Type u_1} (p : α → Prop) [decidable_pred p] (l : list α) :

list ℕ

find_indexes p l is the list of indexes of elements of l that satisfy p.

Equations

list.find_indexes p l = list.foldr_with_index (λ (i : ℕ) (a : α) (is : list ℕ), ite (p a) (i :: is) is) list.nil l

source

def list.indexes_values {α : Type u_1} (p : α → Prop) [decidable_pred p] (l : list α) :

list (ℕ × α)

Returns the elements of l that satisfy p together with their indexes in l. The returned list is ordered by index.

Equations

list.indexes_values p l = list.foldr_with_index (λ (i : ℕ) (a : α) (l : list (ℕ × α)), ite (p a) ((i, a) :: l) l) list.nil l

source

def list.indexes_of {α : Type u_1} [decidable_eq α] (a : α) :

list α → list ℕ

indexes_of a l is the list of all indexes of a in l. For example:

indexes_of a [a, b, a, a] = [0, 2, 3]

Equations

list.indexes_of a = list.find_indexes (eq a)

source

def list.mfoldl_with_index {m : Type v → Type w} [monad m] {α : Type u_1} {β : Type v} (f : ℕ → β → α → m β) (b : β) (as : list α) :

m β

Monadic variant of foldl_with_index.

Equations

list.mfoldl_with_index f b as = list.foldl_with_index (λ (i : ℕ) (ma : m β) (b : α), ma >>= λ (a : β), f i a b) (has_pure.pure b) as

source

def list.mfoldr_with_index {m : Type v → Type w} [monad m] {α : Type u_1} {β : Type v} (f : ℕ → α → β → m β) (b : β) (as : list α) :

m β

Monadic variant of foldr_with_index.

Equations

list.mfoldr_with_index f b as = list.foldr_with_index (λ (i : ℕ) (a : α) (mb : m β), mb >>= λ (b : β), f i a b) (has_pure.pure b) as

source

def list.mmap_with_index_aux {m : Type v → Type w} [applicative m] {α : Type u_1} {β : Type v} (f : ℕ → α → m β) :

ℕ → list α → m (list β)

Auxiliary definition for mmap_with_index.

Equations

list.mmap_with_index_aux f i (a :: as) = list.cons <$> f i a <*> list.mmap_with_index_aux f (i + 1) as
list.mmap_with_index_aux f _x list.nil = has_pure.pure list.nil

source

def list.mmap_with_index {m : Type v → Type w} [applicative m] {α : Type u_1} {β : Type v} (f : ℕ → α → m β) (as : list α) :

m (list β)

Applicative variant of map_with_index.

Equations

list.mmap_with_index f as = list.mmap_with_index_aux f 0 as

source

def list.mmap_with_index'_aux {m : Type v → Type w} [applicative m] {α : Type u_1} (f : ℕ → α → m punit) :

ℕ → list α → m punit

Auxiliary definition for mmap_with_index'.

Equations

list.mmap_with_index'_aux f i (a :: as) = f i a *> list.mmap_with_index'_aux f (i + 1) as
list.mmap_with_index'_aux f _x list.nil = has_pure.pure punit.star

source

def list.mmap_with_index' {m : Type v → Type w} [applicative m] {α : Type u_1} (f : ℕ → α → m punit) (as : list α) :

m punit

A variant of mmap_with_index specialised to applicative actions which return unit.

Equations

list.mmap_with_index' f as = list.mmap_with_index'_aux f 0 as

source

def list.lookmap {α : Type u_1} (f : α → option α) :

list α → list α

lookmap is a combination of lookup and filter_map. lookmap f l will apply f : α → option α to each element of the list, replacing a → b at the first value a in the list such that f a = some b.

Equations

list.lookmap f (a :: l) = list.lookmap._match_1 a l (list.lookmap f l) (f a)
list.lookmap f list.nil = list.nil
list.lookmap._match_1 a l _f_1 (option.some b) = b :: l
list.lookmap._match_1 a l _f_1 option.none = a :: _f_1

source

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

list α → ℕ

countp p l is the number of elements of l that satisfy p.

Equations

list.countp p (x :: xs) = ite (p x) (list.countp p xs).succ (list.countp p xs)
list.countp p list.nil = 0

source

def list.count {α : Type u_1} [decidable_eq α] (a : α) :

list α → ℕ

count a l is the number of occurrences of a in l.

Equations

list.count a = list.countp (eq a)

source

def list.is_prefix {α : Type u_1} (l₁ l₂ : list α) :

Prop

is_prefix l₁ l₂, or l₁ <+: l₂, means that l₁ is a prefix of l₂, that is, l₂ has the form l₁ ++ t for some t.

Equations

l₁ <+: l₂ = ∃ (t : list α), l₁ ++ t = l₂

Instances for list.is_prefix

source

def list.is_suffix {α : Type u_1} (l₁ l₂ : list α) :

Prop

is_suffix l₁ l₂, or l₁ <:+ l₂, means that l₁ is a suffix of l₂, that is, l₂ has the form t ++ l₁ for some t.

Equations

l₁ <:+ l₂ = ∃ (t : list α), t ++ l₁ = l₂

Instances for list.is_suffix

source

def list.is_infix {α : Type u_1} (l₁ l₂ : list α) :

Prop

is_infix l₁ l₂, or l₁ <:+: l₂, means that l₁ is a contiguous substring of l₂, that is, l₂ has the form s ++ l₁ ++ t for some s, t.

Equations

l₁ <:+: l₂ = ∃ (s t : list α), s ++ l₁ ++ t = l₂

Instances for list.is_infix

source

@[simp]

def list.inits {α : Type u_1} :

list α → list (list α)

inits l is the list of initial segments of l.

inits [1, 2, 3] = [[], [1], [1, 2], [1, 2, 3]]

Equations

(a :: l).inits = list.nil :: list.map (λ (t : list α), a :: t) l.inits
list.nil.inits = [list.nil]

source

@[simp]

def list.tails {α : Type u_1} :

list α → list (list α)

tails l is the list of terminal segments of l.

tails [1, 2, 3] = [[1, 2, 3], [2, 3], [3], []]

Equations

(a :: l).tails = (a :: l) :: l.tails
list.nil.tails = [list.nil]

source

def list.sublists'_aux {α : Type u_1} {β : Type u_2} :

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

Equations

(a :: l).sublists'_aux f r = l.sublists'_aux f (l.sublists'_aux (f ∘ list.cons a) r)
list.nil.sublists'_aux f r = f list.nil :: r

source

def list.sublists' {α : Type u_1} (l : list α) :

list (list α)

sublists' l is the list of all (non-contiguous) sublists of l. It differs from sublists only in the order of appearance of the sublists; sublists' uses the first element of the list as the MSB, sublists uses the first element of the list as the LSB.

sublists' [1, 2, 3] = [[], [3], [2], [2, 3], [1], [1, 3], [1, 2], [1, 2, 3]]

Equations

l.sublists' = l.sublists'_aux id list.nil

source

def list.sublists_aux {α : Type u_1} {β : Type u_2} :

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

Equations

(a :: l).sublists_aux f = f [a] (l.sublists_aux (λ (ys : list α) (r : list β), f ys (f (a :: ys) r)))
list.nil.sublists_aux f = list.nil

source

def list.sublists {α : Type u_1} (l : list α) :

list (list α)

sublists l is the list of all (non-contiguous) sublists of l; cf. sublists' for a different ordering.

sublists [1, 2, 3] = [[], [1], [2], [1, 2], [3], [1, 3], [2, 3], [1, 2, 3]]

Equations

l.sublists = list.nil :: l.sublists_aux list.cons

source

def list.sublists_aux₁ {α : Type u_1} {β : Type u_2} :

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

Equations

(a :: l).sublists_aux₁ f = f [a] ++ l.sublists_aux₁ (λ (ys : list α), f ys ++ f (a :: ys))
list.nil.sublists_aux₁ f = list.nil

source

inductive list.forall₂ {α : Type u_1} {β : Type u_2} (R : α → β → Prop) :

list α → list β → Prop

nil : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop}, list.forall₂ R list.nil list.nil
cons : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {a : α} {b : β} {l₁ : list α} {l₂ : list β}, R a b → list.forall₂ R l₁ l₂ → list.forall₂ R (a :: l₁) (b :: l₂)

forall₂ R l₁ l₂ means that l₁ and l₂ have the same length, and whenever a is the nth element of l₁, and b is the nth element of l₂, then R a b is satisfied.

source

@[simp]

def list.all₂ {α : Type u_1} (p : α → Prop) :

list α → Prop

l.all₂ p is equivalent to ∀ a ∈ l, p a, but unfolds directly to a conjunction, i.e. list.all₂ p [0, 1, 2] = p 0 ∧ p 1 ∧ p 2.

Equations

list.all₂ p (x :: hd :: tl) = (p x ∧ list.all₂ p (hd :: tl))
list.all₂ p [x] = p x
list.all₂ p list.nil = true

Instances for list.all₂

list.all₂.decidable_pred

source

def list.transpose_aux {α : Type u_1} :

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

Auxiliary definition used to define transpose. transpose_aux l L takes each element of l and appends it to the start of each element of L.

transpose_aux [a, b, c] [l₁, l₂, l₃] = [a::l₁, b::l₂, c::l₃]

Equations

(a :: i).transpose_aux (l :: ls) = (a :: l) :: i.transpose_aux ls
(a :: i).transpose_aux list.nil = [a] :: i.transpose_aux list.nil
list.nil.transpose_aux ls = ls

source

def list.transpose {α : Type u_1} :

list (list α) → list (list α)

transpose of a list of lists, treated as a matrix.

transpose [[1, 2], [3, 4], [5, 6]] = [[1, 3, 5], [2, 4, 6]]

Equations

(l :: ls).transpose = l.transpose_aux ls.transpose
list.nil.transpose = list.nil

source

def list.sections {α : Type u_1} :

list (list α) → list (list α)

List of all sections through a list of lists. A section of [L₁, L₂, ..., Lₙ] is a list whose first element comes from L₁, whose second element comes from L₂, and so on.

Equations

(l :: L).sections = L.sections >>= λ (s : list α), list.map (λ (a : α), a :: s) l
list.nil.sections = [list.nil]

source

def list.permutations_aux2 {α : Type u_1} {β : Type u_2} (t : α) (ts : list α) (r : list β) :

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

An auxiliary function for defining permutations. permutations_aux2 t ts r ys f is equal to (ys ++ ts, (insert_left ys t ts).map f ++ r), where insert_left ys t ts (not explicitly defined) is the list of lists of the form insert_nth n t (ys ++ ts) for 0 ≤ n < length ys.

permutations_aux2 10 [4, 5, 6] [] [1, 2, 3] id =
  ([1, 2, 3, 4, 5, 6],
   [[10, 1, 2, 3, 4, 5, 6],
    [1, 10, 2, 3, 4, 5, 6],
    [1, 2, 10, 3, 4, 5, 6]])

Equations

list.permutations_aux2 t ts r (y :: ys) f = list.permutations_aux2._match_1 t y f (list.permutations_aux2 t ts r ys (λ (x : list α), f (y :: x)))
list.permutations_aux2 t ts r list.nil f = (ts, r)
list.permutations_aux2._match_1 t y f (us, zs) = (y :: us, f (t :: y :: us) :: zs)

source

def list.permutations_aux.rec {α : Type u_1} {C : list α → list α → Sort v} (H0 : Π (is : list α), C list.nil is) (H1 : Π (t : α) (ts is : list α), C ts (t :: is) → C is list.nil → C (t :: ts) is) (l₁ l₂ : list α) :

C l₁ l₂

A recursor for pairs of lists. To have C l₁ l₂ for all l₁, l₂, it suffices to have it for l₂ = [] and to be able to pour the elements of l₁ into l₂.

Equations

list.permutations_aux.rec H0 H1 (t :: ts) is = H1 t ts is (list.permutations_aux.rec H0 H1 ts (t :: is)) (list.permutations_aux.rec H0 H1 is list.nil)
list.permutations_aux.rec H0 H1 list.nil is = H0 is

source

def list.permutations_aux {α : Type u_1} :

list α → list α → list (list α)

An auxiliary function for defining permutations. permutations_aux ts is is the set of all permutations of is ++ ts that do not fix ts.

Equations

list.permutations_aux = list.permutations_aux.rec (λ (is : list α), list.nil) (λ (t : α) (ts is : list α) (IH1 : (λ (_x _x : list α), list (list α)) ts (t :: is)) (IH2 : (λ (_x _x : list α), list (list α)) is list.nil), list.foldr (λ (y : list α) (r : (λ (_x _x : list α), list (list α)) (t :: ts) is), (list.permutations_aux2 t ts r y id).snd) IH1 (is :: IH2))

source

def list.permutations {α : Type u_1} (l : list α) :

list (list α)

List of all permutations of l.

permutations [1, 2, 3] =
  [[1, 2, 3], [2, 1, 3], [3, 2, 1],
   [2, 3, 1], [3, 1, 2], [1, 3, 2]]

Equations

l.permutations = l :: l.permutations_aux list.nil

source

@[simp]

def list.permutations'_aux {α : Type u_1} (t : α) :

list α → list (list α)

permutations'_aux t ts inserts t into every position in ts, including the last. This function is intended for use in specifications, so it is simpler than permutations_aux2, which plays roughly the same role in permutations.

Note that (permutations_aux2 t [] [] ts id).2 is similar to this function, but skips the last position:

permutations'_aux 10 [1, 2, 3] =
  [[10, 1, 2, 3], [1, 10, 2, 3], [1, 2, 10, 3], [1, 2, 3, 10]]
(permutations_aux2 10 [] [] [1, 2, 3] id).2 =
  [[10, 1, 2, 3], [1, 10, 2, 3], [1, 2, 10, 3]]

Equations

list.permutations'_aux t (y :: ys) = (t :: y :: ys) :: list.map (list.cons y) (list.permutations'_aux t ys)
list.permutations'_aux t list.nil = [[t]]

source

@[simp]

def list.permutations' {α : Type u_1} :

list α → list (list α)

List of all permutations of l. This version of permutations is less efficient but has simpler definitional equations. The permutations are in a different order, but are equal up to permutation, as shown by list.permutations_perm_permutations'.

 permutations [1, 2, 3] =
   [[1, 2, 3], [2, 1, 3], [2, 3, 1],
    [1, 3, 2], [3, 1, 2], [3, 2, 1]]

Equations

(t :: ts).permutations' = ts.permutations'.bind (list.permutations'_aux t)
list.nil.permutations' = [list.nil]

source

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

list α → list α

erasep p l removes the first element of l satisfying the predicate p.

Equations

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

source

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

list α → option α × list α

extractp p l returns a pair of an element a of l satisfying the predicate p, and l, with a removed. If there is no such element a it returns (none, l).

Equations

list.extractp p (a :: l) = ite (p a) (option.some a, l) (list.extractp._match_1 a (list.extractp p l))
list.extractp p list.nil = (option.none α, list.nil α)
list.extractp._match_1 a (a', l') = (a', a :: l')

source

def list.revzip {α : Type u_1} (l : list α) :

list (α × α)

revzip l returns a list of pairs of the elements of l paired with the elements of l in reverse order.

revzip [1,2,3,4,5] = [(1, 5), (2, 4), (3, 3), (4, 2), (5, 1)]

Equations

l.revzip = l.zip l.reverse

source

def list.product {α : Type u_1} {β : Type u_2} (l₁ : list α) (l₂ : list β) :

list (α × β)

product l₁ l₂ is the list of pairs (a, b) where a ∈ l₁ and b ∈ l₂.

product [1, 2] [5, 6] = [(1, 5), (1, 6), (2, 5), (2, 6)]

Equations

l₁ ×ˢ l₂ = l₁.bind (λ (a : α), list.map (prod.mk a) l₂)

source

@[protected]

def list.sigma {α : Type u_1} {σ : α → Type u_2} (l₁ : list α) (l₂ : Π (a : α), list (σ a)) :

list (Σ (a : α), σ a)

sigma l₁ l₂ is the list of dependent pairs (a, b) where a ∈ l₁ and b ∈ l₂ a.

sigma [1, 2] (λ_, [(5 : ℕ), 6]) = [(1, 5), (1, 6), (2, 5), (2, 6)]

Equations

l₁.sigma l₂ = l₁.bind (λ (a : α), list.map (sigma.mk a) (l₂ a))

source

def list.of_fn_aux {α : Type u_1} {n : ℕ} (f : fin n → α) (m : ℕ) :

m ≤ n → list α → list α

Auxliary definition used to define of_fn.

of_fn_aux f m h l returns the first m elements of of_fn f appended to l

Equations

list.of_fn_aux f m.succ h l = list.of_fn_aux f m _ (f ⟨m, h⟩ :: l)
list.of_fn_aux f 0 h l = l

source

def list.of_fn {α : Type u_1} {n : ℕ} (f : fin n → α) :

list α

of_fn f with f : fin n → α returns the list whose ith element is f i of_fun f = [f 0, f 1, ... , f(n - 1)]

Equations

list.of_fn f = list.of_fn_aux f n list.of_fn._proof_1 list.nil

source

def list.of_fn_nth_val {α : Type u_1} {n : ℕ} (f : fin n → α) (i : ℕ) :

option α

of_fn_nth_val f i returns some (f i) if i < n and none otherwise.

Equations

list.of_fn_nth_val f i = dite (i < n) (λ (h : i < n), option.some (f ⟨i, h⟩)) (λ (h : ¬i < n), option.none)

source

def list.disjoint {α : Type u_1} (l₁ l₂ : list α) :

Prop

disjoint l₁ l₂ means that l₁ and l₂ have no elements in common.

Equations

l₁.disjoint l₂ = ∀ ⦃a : α⦄, a ∈ l₁ → a ∈ l₂ → false

source

inductive list.pairwise {α : Type u_1} (R : α → α → Prop) :

list α → Prop

nil : ∀ {α : Type u_1} {R : α → α → Prop}, list.pairwise R list.nil
cons : ∀ {α : Type u_1} {R : α → α → Prop} {a : α} {l : list α}, (∀ (a' : α), a' ∈ l → R a a') → list.pairwise R l → list.pairwise R (a :: l)

pairwise R l means that all the elements with earlier indexes are R-related to all the elements with later indexes.

pairwise R [1, 2, 3] ↔ R 1 2 ∧ R 1 3 ∧ R 2 3

For example if R = (≠) then it asserts l has no duplicates, and if R = (<) then it asserts that l is (strictly) sorted.

Instances for list.pairwise

list.decidable_pairwise

source

@[simp]

theorem list.pairwise_cons {α : Type u_1} {R : α → α → Prop} {a : α} {l : list α} :

list.pairwise R (a :: l) ↔ (∀ (a' : α), a' ∈ l → R a a') ∧ list.pairwise R l

source

@[protected, instance]

def list.decidable_pairwise {α : Type u_1} {R : α → α → Prop} [decidable_rel R] (l : list α) :

decidable (list.pairwise R l)

Equations

l.decidable_pairwise = list.rec (decidable.is_true list.pairwise.nil) (λ (hd : α) (tl : list α) (ih : decidable (list.pairwise R tl)), decidable_of_iff' ((∀ (a' : α), a' ∈ tl → R hd a') ∧ list.pairwise R tl) list.pairwise_cons) l

source

def list.pw_filter {α : Type u_1} (R : α → α → Prop) [decidable_rel R] :

list α → list α

pw_filter R l is a maximal sublist of l which is pairwise R. pw_filter (≠) is the erase duplicates function (cf. dedup), and pw_filter (<) finds a maximal increasing subsequence in l. For example,

pw_filter (<) [0, 1, 5, 2, 6, 3, 4] = [0, 1, 2, 3, 4]

Equations

list.pw_filter R (x :: xs) = let IH : list α := list.pw_filter R xs in ite (∀ (y : α), y ∈ IH → R x y) (x :: IH) IH
list.pw_filter R list.nil = list.nil

source

inductive list.chain {α : Type u_1} (R : α → α → Prop) :

α → list α → Prop

nil : ∀ {α : Type u_1} {R : α → α → Prop} {a : α}, list.chain R a list.nil
cons : ∀ {α : Type u_1} {R : α → α → Prop} {a b : α} {l : list α}, R a b → list.chain R b l → list.chain R a (b :: l)

chain R a l means that R holds between adjacent elements of a::l.

chain R a [b, c, d] ↔ R a b ∧ R b c ∧ R c d

Instances for list.chain

list.decidable_chain

source

def list.chain' {α : Type u_1} (R : α → α → Prop) :

list α → Prop

chain' R l means that R holds between adjacent elements of l.

chain' R [a, b, c, d] ↔ R a b ∧ R b c ∧ R c d

Equations

list.chain' R (a :: l) = list.chain R a l
list.chain' R list.nil = true

Instances for list.chain'

list.decidable_chain'

source

@[simp]

theorem list.chain_cons {α : Type u_1} {R : α → α → Prop} {a b : α} {l : list α} :

list.chain R a (b :: l) ↔ R a b ∧ list.chain R b l

source

@[protected, instance]

def list.decidable_chain {α : Type u_1} {R : α → α → Prop} [decidable_rel R] (a : α) (l : list α) :

decidable (list.chain R a l)

Equations

list.decidable_chain a l = list.rec (λ (a : α), _.mpr decidable.true) (λ (l_hd : α) (l_tl : list α) (l_ih : Π (a : α), decidable (list.chain R a l_tl)) (a : α), _.mpr and.decidable) l a

source

@[protected, instance]

def list.decidable_chain' {α : Type u_1} {R : α → α → Prop} [decidable_rel R] (l : list α) :

decidable (list.chain' R l)

Equations

l.decidable_chain' = l.cases_on (id decidable.true) (λ (l_hd : α) (l_tl : list α), id (list.decidable_chain l_hd l_tl))

source

def list.nodup {α : Type u_1} :

list α → Prop

nodup l means that l has no duplicates, that is, any element appears at most once in the list. It is defined as pairwise (≠).

Equations

list.nodup = list.pairwise ne

Instances for list.nodup

list.nodup_decidable

source

@[protected, instance]

def list.nodup_decidable {α : Type u_1} [decidable_eq α] (l : list α) :

decidable l.nodup

Equations

list.nodup_decidable = list.decidable_pairwise

source

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

list α → list α

dedup l removes duplicates from l (taking only the last occurrence). Defined as pw_filter (≠).

dedup [1, 0, 2, 2, 1] = [0, 2, 1]

Equations

list.dedup = list.pw_filter ne

source

def list.destutter' {α : Type u_1} (R : α → α → Prop) [decidable_rel R] :

α → list α → list α

Greedily create a sublist of a :: l such that, for every two adjacent elements a, b, R a b holds. Mostly used with ≠; for example, destutter' (≠) 1 [2, 2, 1, 1] = [1, 2, 1], destutter' (≠) 1, [2, 3, 3] = [1, 2, 3], destutter' (<) 1 [2, 5, 2, 3, 4, 9] = [1, 2, 5, 9].

Equations

list.destutter' R a (h :: l) = ite (R a h) (a :: list.destutter' R h l) (list.destutter' R a l)
list.destutter' R a list.nil = [a]

source

def list.destutter {α : Type u_1} (R : α → α → Prop) [decidable_rel R] :

list α → list α

Greedily create a sublist of l such that, for every two adjacent elements a, b ∈ l, R a b holds. Mostly used with ≠; for example, destutter (≠) [1, 2, 2, 1, 1] = [1, 2, 1], destutter (≠) [1, 2, 3, 3] = [1, 2, 3], destutter (<) [1, 2, 5, 2, 3, 4, 9] = [1, 2, 5, 9].

Equations

list.destutter R (h :: l) = list.destutter' R h l
list.destutter R list.nil = list.nil

source

@[simp]

def list.range' :

ℕ → ℕ → list ℕ

range' s n is the list of numbers [s, s+1, ..., s+n-1]. It is intended mainly for proving properties of range and iota.

Equations

list.range' s (n + 1) = s :: list.range' (s + 1) n
list.range' s 0 = list.nil

source

def list.reduce_option {α : Type u_1} :

list (option α) → list α

Drop nones from a list, and replace each remaining some a with a.

Equations

list.reduce_option = list.filter_map id

source

@[simp]

def list.ilast' {α : Type u_1} :

α → list α → α

ilast' x xs returns the last element of xs if xs is non-empty; it returns x otherwise

Equations

list.ilast' a (b :: l) = list.ilast' b l
list.ilast' a list.nil = a

source

@[simp]

def list.last' {α : Type u_1} :

list α → option α

last' xs returns the last element of xs if xs is non-empty; it returns none otherwise

Equations

(b :: hd :: tl).last' = (hd :: tl).last'
[a].last' = option.some a
list.nil.last' = option.none

source

def list.rotate {α : Type u_1} (l : list α) (n : ℕ) :

list α

rotate l n rotates the elements of l to the left by n

rotate [0, 1, 2, 3, 4, 5] 2 = [2, 3, 4, 5, 0, 1]

Equations

l.rotate n = list.rotate._match_1 (list.split_at (n % l.length) l)
list.rotate._match_1 (l₁, l₂) = l₂ ++ l₁

source

def list.rotate' {α : Type u_1} :

list α → ℕ → list α

rotate' is the same as rotate, but slower. Used for proofs about rotate

Equations

(a :: l).rotate' (n + 1) = (l ++ [a]).rotate' n
(hd :: tl).rotate' 0 = hd :: tl
list.nil.rotate' n.succ = list.nil
list.nil.rotate' 0 = list.nil

source

def list.choose_x {α : Type u_1} (p : α → Prop) [decidable_pred p] (l : list α) (hp : ∃ (a : α), a ∈ l ∧ p a) :

{a // a ∈ l ∧ p a}

Given a decidable predicate p and a proof of existence of a ∈ l such that p a, choose the first element with this property. This version returns both a and proofs of a ∈ l and p a.

Equations

list.choose_x p (l :: ls) hp = dite (p l) (λ (pl : p l), ⟨l, _⟩) (λ (pl : ¬p l), list.choose_x._match_2 p l ls (list.choose_x p ls _))
list.choose_x p list.nil hp = _.elim
list.choose_x._match_2 p l ls ⟨a, _⟩ = ⟨a, _⟩

source

def list.choose {α : Type u_1} (p : α → Prop) [decidable_pred p] (l : list α) (hp : ∃ (a : α), a ∈ l ∧ p a) :

α

Given a decidable predicate p and a proof of existence of a ∈ l such that p a, choose the first element with this property. This version returns a : α, and properties are given by choose_mem and choose_property.

Equations

list.choose p l hp = ↑(list.choose_x p l hp)

source

def list.mmap_filter {m : Type → Type v} [monad m] {α : Type u_1} {β : Type} (f : α → m (option β)) :

list α → m (list β)

Filters and maps elements of a list

Equations

list.mmap_filter f (h :: t) = f h >>= λ (b : option β), list.mmap_filter f t >>= λ (t' : list β), return (list.mmap_filter._match_1 t' b)
list.mmap_filter f list.nil = return list.nil
list.mmap_filter._match_1 t' (option.some x) = x :: t'
list.mmap_filter._match_1 t' option.none = t'

source

def list.mmap_upper_triangle {m : Type u → Type u_1} [monad m] {α β : Type u} (f : α → α → m β) :

list α → m (list β)

mmap_upper_triangle f l calls f on all elements in the upper triangular part of l × l. That is, for each e ∈ l, it will run f e e and then f e e' for each e' that appears after e in l.

Example: suppose l = [1, 2, 3]. mmap_upper_triangle f l will produce the list [f 1 1, f 1 2, f 1 3, f 2 2, f 2 3, f 3 3].

Equations

list.mmap_upper_triangle f (h :: t) = f h h >>= λ (v : β), list.mmap (f h) t >>= λ (l : list β), list.mmap_upper_triangle f t >>= λ (t : list β), return (v :: l ++ t)
list.mmap_upper_triangle f list.nil = return list.nil

source

def list.mmap'_diag {m : Type → Type u_1} [monad m] {α : Type u_2} (f : α → α → m unit) :

list α → m unit

mmap'_diag f l calls f on all elements in the upper triangular part of l × l. That is, for each e ∈ l, it will run f e e and then f e e' for each e' that appears after e in l.

Example: suppose l = [1, 2, 3]. mmap'_diag f l will evaluate, in this order, f 1 1, f 1 2, f 1 3, f 2 2, f 2 3, f 3 3.

Equations

list.mmap'_diag f (h :: t) = f h h >> list.mmap' (f h) t >> list.mmap'_diag f t
list.mmap'_diag f list.nil = return unit.star()

source

@[protected]

def list.traverse {F : Type u → Type v} [applicative F] {α : Type u_1} {β : Type u} (f : α → F β) :

list α → F (list β)

Equations

list.traverse f (x :: xs) = list.cons <$> f x <*> list.traverse f xs
list.traverse f list.nil = has_pure.pure list.nil

source

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

list α → list α → option (list α)

get_rest l l₁ returns some l₂ if l = l₁ ++ l₂. If l₁ is not a prefix of l, returns none

Equations

(x :: l).get_rest (y :: l₁) = ite (x = y) (l.get_rest l₁) option.none
(hd :: tl).get_rest list.nil = option.some (hd :: tl)
list.nil.get_rest (hd :: tl) = option.none
list.nil.get_rest list.nil = option.some list.nil

source

def list.slice {α : Type u_1} :

ℕ → ℕ → list α → list α

list.slice n m xs removes a slice of length m at index n in list xs.

Equations

list.slice n.succ m (x :: xs) = x :: list.slice n m xs
list.slice n.succ m list.nil = list.nil
list.slice 0 n xs = list.drop n xs

source

@[simp]

def list.map₂_left' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → option β → γ) :

list α → list β → list γ × list β

Left-biased version of list.map₂. map₂_left' f as bs applies f to each pair of elements aᵢ ∈ as and bᵢ ∈ bs. If bs is shorter than as, f is applied to none for the remaining aᵢ. Returns the results of the f applications and the remaining bs.

map₂_left' prod.mk [1, 2] ['a'] = ([(1, some 'a'), (2, none)], [])

map₂_left' prod.mk [1] ['a', 'b'] = ([(1, some 'a')], ['b'])
```

Equations

list.map₂_left' f (a :: as) (b :: bs) = let rec : list γ × list β := list.map₂_left' f as bs in (f a (option.some b) :: rec.fst, rec.snd)
list.map₂_left' f (a :: as) list.nil = (list.map (λ (a : α), f a option.none) (a :: as), list.nil β)
list.map₂_left' f list.nil bs = (list.nil γ, bs)

source

def list.map₂_right' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : option α → β → γ) (as : list α) (bs : list β) :

list γ × list α

Right-biased version of list.map₂. map₂_right' f as bs applies f to each pair of elements aᵢ ∈ as and bᵢ ∈ bs. If as is shorter than bs, f is applied to none for the remaining bᵢ. Returns the results of the f applications and the remaining as.

map₂_right' prod.mk [1] ['a', 'b'] = ([(some 1, 'a'), (none, 'b')], [])

map₂_right' prod.mk [1, 2] ['a'] = ([(some 1, 'a')], [2])
```

Equations

list.map₂_right' f as bs = list.map₂_left' (flip f) bs as

source

def list.zip_left' {α : Type u_1} {β : Type u_2} :

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

Left-biased version of list.zip. zip_left' as bs returns the list of pairs (aᵢ, bᵢ) for aᵢ ∈ as and bᵢ ∈ bs. If bs is shorter than as, the remaining aᵢ are paired with none. Also returns the remaining bs.

zip_left' [1, 2] ['a'] = ([(1, some 'a'), (2, none)], [])

zip_left' [1] ['a', 'b'] = ([(1, some 'a')], ['b'])

zip_left' = map₂_left' prod.mk

```

Equations

list.zip_left' = list.map₂_left' prod.mk

source

def list.zip_right' {α : Type u_1} {β : Type u_2} :

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

Right-biased version of list.zip. zip_right' as bs returns the list of pairs (aᵢ, bᵢ) for aᵢ ∈ as and bᵢ ∈ bs. If as is shorter than bs, the remaining bᵢ are paired with none. Also returns the remaining as.

zip_right' [1] ['a', 'b'] = ([(some 1, 'a'), (none, 'b')], [])

zip_right' [1, 2] ['a'] = ([(some 1, 'a')], [2])

zip_right' = map₂_right' prod.mk
```

Equations

list.zip_right' = list.map₂_right' prod.mk

source

@[simp]

def list.map₂_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → option β → γ) :

list α → list β → list γ

Left-biased version of list.map₂. map₂_left f as bs applies f to each pair aᵢ ∈ as and bᵢ ‌∈ bs. If bs is shorter than as, f is applied to none for the remaining aᵢ.

map₂_left prod.mk [1, 2] ['a'] = [(1, some 'a'), (2, none)]

map₂_left prod.mk [1] ['a', 'b'] = [(1, some 'a')]

map₂_left f as bs = (map₂_left' f as bs).fst
```

Equations

list.map₂_left f (a :: as) (b :: bs) = f a (option.some b) :: list.map₂_left f as bs
list.map₂_left f (a :: as) list.nil = list.map (λ (a : α), f a option.none) (a :: as)
list.map₂_left f list.nil _x = list.nil

source

def list.map₂_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : option α → β → γ) (as : list α) (bs : list β) :

list γ

Right-biased version of list.map₂. map₂_right f as bs applies f to each pair aᵢ ∈ as and bᵢ ‌∈ bs. If as is shorter than bs, f is applied to none for the remaining bᵢ.

map₂_right prod.mk [1, 2] ['a'] = [(some 1, 'a')]

map₂_right prod.mk [1] ['a', 'b'] = [(some 1, 'a'), (none, 'b')]

map₂_right f as bs = (map₂_right' f as bs).fst
```

Equations

list.map₂_right f as bs = list.map₂_left (flip f) bs as

source

def list.zip_left {α : Type u_1} {β : Type u_2} :

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

Left-biased version of list.zip. zip_left as bs returns the list of pairs (aᵢ, bᵢ) for aᵢ ∈ as and bᵢ ∈ bs. If bs is shorter than as, the remaining aᵢ are paired with none.

zip_left [1, 2] ['a'] = [(1, some 'a'), (2, none)]

zip_left [1] ['a', 'b'] = [(1, some 'a')]

zip_left = map₂_left prod.mk
```

Equations

list.zip_left = list.map₂_left prod.mk

source

def list.zip_right {α : Type u_1} {β : Type u_2} :

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

Right-biased version of list.zip. zip_right as bs returns the list of pairs (aᵢ, bᵢ) for aᵢ ∈ as and bᵢ ∈ bs. If as is shorter than bs, the remaining bᵢ are paired with none.

zip_right [1, 2] ['a'] = [(some 1, 'a')]

zip_right [1] ['a', 'b'] = [(some 1, 'a'), (none, 'b')]

zip_right = map₂_right prod.mk
```

Equations

list.zip_right = list.map₂_right prod.mk

source

def list.all_some {α : Type u_1} :

list (option α) → option (list α)

If all elements of xs are some xᵢ, all_some xs returns the xᵢ. Otherwise it returns none.

all_some [some 1, some 2] = some [1, 2]
all_some [some 1, none  ] = none

Equations

(option.some a :: as).all_some = list.cons a <$> as.all_some
(option.none :: as).all_some = option.none
list.nil.all_some = option.some list.nil

source

def list.fill_nones {α : Type u_1} :

list (option α) → list α → list α

fill_nones xs ys replaces the nones in xs with elements of ys. If there are not enough ys to replace all the nones, the remaining nones are dropped from xs.

fill_nones [none, some 1, none, none] [2, 3] = [2, 1, 3]

Equations

(option.some a :: as).fill_nones as' = a :: as.fill_nones as'
(option.none :: as).fill_nones (a :: as') = a :: as.fill_nones as'
(option.none :: as).fill_nones list.nil = as.reduce_option
list.nil.fill_nones _x = list.nil

source

def list.take_list {α : Type u_1} :

list α → list ℕ → list (list α) × list α

take_list as ns extracts successive sublists from as. For ns = n₁ ... nₘ, it first takes the n₁ initial elements from as, then the next n₂ ones, etc. It returns the sublists of as -- one for each nᵢ -- and the remaining elements of as. If as does not have at least as many elements as the sum of the nᵢ, the corresponding sublists will have less than nᵢ elements.

take_list ['a', 'b', 'c', 'd', 'e'] [2, 1, 1] = ([['a', 'b'], ['c'], ['d']], ['e'])
take_list ['a', 'b'] [3, 1] = ([['a', 'b'], []], [])

Equations

xs.take_list (n :: ns) = list.take_list._match_2 (λ (xs₂ : list α), xs₂.take_list ns) (list.split_at n xs)
xs.take_list list.nil = (list.nil (list α), xs)
list.take_list._match_2 _f_1 (xs₁, xs₂) = list.take_list._match_1 xs₁ (_f_1 xs₂)
list.take_list._match_1 xs₁ (xss, rest) = (xs₁ :: xss, rest)

source

def list.to_rbmap {α : Type u_1} :

list α → rbmap ℕ α has_lt.lt

to_rbmap as is the map that associates each index i of as with the corresponding element of as.

to_rbmap ['a', 'b', 'c'] = rbmap_of [(0, 'a'), (1, 'b'), (2, 'c')]

Equations

list.to_rbmap = list.foldl_with_index (λ (i : ℕ) (mapp : rbmap ℕ α has_lt.lt) (a : α), mapp.insert i a) (mk_rbmap ℕ α has_lt.lt)

source

def list.to_chunks_aux {α : Type u_1} (n : ℕ) :

list α → ℕ → list α × list (list α)

Auxliary definition used to define to_chunks.

to_chunks_aux n xs i returns (xs.take i, (xs.drop i).to_chunks (n+1)), that is, the first i elements of xs, and the remaining elements chunked into sublists of length n+1.

Equations

list.to_chunks_aux n (x :: xs) (i + 1) = list.to_chunks_aux._match_2 x (list.to_chunks_aux n xs i)
list.to_chunks_aux n (x :: xs) 0 = list.to_chunks_aux._match_1 x (list.to_chunks_aux n xs n)
list.to_chunks_aux n list.nil i = (list.nil α, list.nil (list α))
list.to_chunks_aux._match_2 x (l, L) = (x :: l, L)
list.to_chunks_aux._match_1 x (l, L) = (list.nil α, (x :: l) :: L)

source

def list.to_chunks {α : Type u_1} :

ℕ → list α → list (list α)

xs.to_chunks n splits the list into sublists of size at most n, such that (xs.to_chunks n).join = xs.

[1, 2, 3, 4, 5, 6, 7, 8].to_chunks 10 = [[1, 2, 3, 4, 5, 6, 7, 8]]
[1, 2, 3, 4, 5, 6, 7, 8].to_chunks 3 = [[1, 2, 3], [4, 5, 6], [7, 8]]
[1, 2, 3, 4, 5, 6, 7, 8].to_chunks 2 = [[1, 2], [3, 4], [5, 6], [7, 8]]
[1, 2, 3, 4, 5, 6, 7, 8].to_chunks 0 = [[1, 2, 3, 4, 5, 6, 7, 8]]

Equations

list.to_chunks (n + 1) (x :: xs) = list.to_chunks._match_1 x (list.to_chunks_aux n xs n)
list.to_chunks n.succ list.nil = list.nil
list.to_chunks 0 (hd :: tl) = [hd :: tl]
list.to_chunks 0 list.nil = list.nil
list.to_chunks._match_1 x (l, L) = (x :: l) :: L

source

meta def list.map_async_chunked {α : Type u_1} {β : Type u_2} (f : α → β) (xs : list α) (chunk_size : ℕ := 1024) :

list β

Asynchronous version of list.map.

source

def list.zip_with3 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β → γ → δ) :

list α → list β → list γ → list δ

Ternary version of list.zip_with.

Equations

list.zip_with3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: list.zip_with3 f xs ys zs
list.zip_with3 f (hd :: tl) (hd_1 :: tl_1) list.nil = list.nil
list.zip_with3 f (hd :: tl) list.nil _x = list.nil
list.zip_with3 f list.nil _x _x_1 = list.nil

source

def list.zip_with4 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} (f : α → β → γ → δ → ε) :

list α → list β → list γ → list δ → list ε

Quaternary version of list.zip_with.

Equations

list.zip_with4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: list.zip_with4 f xs ys zs us
list.zip_with4 f (hd :: tl) (hd_1 :: tl_1) (hd_2 :: tl_2) list.nil = list.nil
list.zip_with4 f (hd :: tl) (hd_1 :: tl_1) list.nil _x = list.nil
list.zip_with4 f (hd :: tl) list.nil _x _x_1 = list.nil
list.zip_with4 f list.nil _x _x_1 _x_2 = list.nil

source

def list.zip_with5 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} {ζ : Type u_6} (f : α → β → γ → δ → ε → ζ) :

list α → list β → list γ → list δ → list ε → list ζ

Quinary version of list.zip_with.

Equations

list.zip_with5 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) = f x y z u v :: list.zip_with5 f xs ys zs us vs
list.zip_with5 f (hd :: tl) (hd_1 :: tl_1) (hd_2 :: tl_2) (hd_3 :: tl_3) list.nil = list.nil
list.zip_with5 f (hd :: tl) (hd_1 :: tl_1) (hd_2 :: tl_2) list.nil _x = list.nil
list.zip_with5 f (hd :: tl) (hd_1 :: tl_1) list.nil _x _x_1 = list.nil
list.zip_with5 f (hd :: tl) list.nil _x _x_1 _x_2 = list.nil
list.zip_with5 f list.nil _x _x_1 _x_2 _x_3 = list.nil

source

def list.replace_if {α : Type u_1} :

list α → list bool → list α → list α

Given a starting list old, a list of booleans and a replacement list new, read the items in old in succession and either replace them with the next element of new or not, according as to whether the corresponding boolean is tt or ff.

Equations

(n :: ns).replace_if (tf :: bs) (c :: cs) = ite ↥tf (c :: ns.replace_if bs cs) (n :: ns.replace_if bs (c :: cs))
(hd :: tl).replace_if (hd_1 :: tl_1) list.nil = hd :: tl
(hd :: tl).replace_if list.nil (hd_1 :: tl_1) = hd :: tl
(hd :: tl).replace_if list.nil list.nil = hd :: tl
list.nil.replace_if (hd :: tl) (hd_1 :: tl_1) = list.nil
list.nil.replace_if (hd :: tl) list.nil = list.nil
list.nil.replace_if list.nil (hd :: tl) = list.nil
list.nil.replace_if list.nil list.nil = list.nil

source

def list.map_with_prefix_suffix_aux {α : Type u_1} {β : Type u_2} (f : list α → α → list α → β) :

list α → list α → list β

An auxiliary function for list.map_with_prefix_suffix.

Equations

list.map_with_prefix_suffix_aux f prev (h :: t) = f prev h t :: list.map_with_prefix_suffix_aux f (prev.concat h) t
list.map_with_prefix_suffix_aux f prev list.nil = list.nil

source

def list.map_with_prefix_suffix {α : Type u_1} {β : Type u_2} (f : list α → α → list α → β) (l : list α) :

list β

list.map_with_prefix_suffix f l maps f across a list l. For each a ∈ l with l = pref ++ [a] ++ suff, a is mapped to f pref a suff.

Example: if f : list ℕ → ℕ → list ℕ → β, list.map_with_prefix_suffix f [1, 2, 3] will produce the list [f [] 1 [2, 3], f [1] 2 [3], f [1, 2] 3 []].

Equations

list.map_with_prefix_suffix f l = list.map_with_prefix_suffix_aux f list.nil l

source

def list.map_with_complement {α : Type u_1} {β : Type u_2} (f : α → list α → β) :

list α → list β

list.map_with_complement f l is a variant of list.map_with_prefix_suffix that maps f across a list l. For each a ∈ l with l = pref ++ [a] ++ suff, a is mapped to f a (pref ++ suff), i.e., the list input to f is l with a removed.

Example: if f : ℕ → list ℕ → β, list.map_with_complement f [1, 2, 3] will produce the list [f 1 [2, 3], f 2 [1, 3], f 3 [1, 2]].

Equations

list.map_with_complement f = list.map_with_prefix_suffix (λ (pref : list α) (a : α) (suff : list α), f a (pref ++ suff))

mathlib3 documentation

Definitions on lists #