# mathlibdocumentation

data.list.defs

## Definitions on lists #

This file contains various definitions on lists. It does not contain proofs about these definitions, those are contained in other files in `data/list`

@[protected, instance]
def list.has_sdiff {α : Type u_1} [decidable_eq α] :
Equations
def list.split_at {α : Type u_1} :

Split a list at an index.

``````split_at 2 [a, b, c] = ([a, b], [c])
``````
Equations
def list.split_on_p_aux {α : Type u} (P : α Prop)  :
list α (list α list α) list (list α)

An auxiliary function for `split_on_p`.

Equations
def list.split_on_p {α : Type u} (P : α Prop) (l : list α) :
list (list α)

Split a list at every element satisfying a predicate.

Equations
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
@[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
@[simp]
def list.head' {α : Type u_1} :
list α

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

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

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

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

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

Equations
• (x :: xs) (n + 1) = xs n
• (x :: xs) 0 = x
• _x = d
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
@[simp]
def list.modify_nth_tail {α : Type u_1} (f : 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
@[simp]
def list.modify_head {α : Type u_1} (f : α α) :
list α list α

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

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

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

Equations
@[simp]
def list.modify_last {α : Type u_1} (f : α α) :
list α list α

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

Equations
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
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
def list.take_while {α : Type u_1} (p : α Prop)  :
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
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
• a (b :: l) = a :: (f a b) l
• = [a]
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
• (a :: l) = list.scanr_aux._match_1 f a b l)
• = (b, list.nil β)
• list.scanr_aux._match_1 f a (b', l') = (f a b', b' :: l')
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
• b l = list.scanr._match_1 b l)
• list.scanr._match_1 (b', l') = b' :: l'
def list.prod {α : Type u_1} [has_mul α] [has_one α] :
list α α

Product of a list.

``````prod [a, b, c] = ((1 * a) * b) * c
``````
Equations
def list.sum {α : Type u_1} [has_add α] [has_zero α] :
list α α

Sum of a list.

``````sum [a, b, c] = ((0 + a) + b) + c
``````
Equations
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
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
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
def list.find {α : Type u_1} (p : α Prop)  :
list α

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

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

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

Equations
def list.mbfind' {m : Type u Type v} [monad m] {α : Type u} (p : α m ) :
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
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
def list.many {m : Type Type v} [monad m] {α : Type u} (p : α 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
def list.mall {m : Type Type v} [monad m] {α : Type u} (p : α m bool) (as : list α) :

`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
def list.mbor {m : Type Type v} [monad m] :

`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
def list.mband {m : Type Type v} [monad m] :

`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
def list.foldl_with_index_aux {α : Type u_1} {β : Type u_2} (f : α β α) :
α list β α

Auxiliary definition for `foldl_with_index`.

Equations
• (b :: l) = (i + 1) (f i a b) l
• = a
def list.foldl_with_index {α : Type 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
• = l
def list.foldr_with_index_aux {α : Type u_1} {β : Type u_2} (f : α β β) :
β list α β

Auxiliary definition for `foldr_with_index`.

Equations
• (a :: l) = f i a (i + 1) b l)
• = b
def list.foldr_with_index {α : Type u_1} {β : Type 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
• = l
def list.find_indexes {α : Type u_1} (p : α Prop) (l : list α) :

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

Equations
def list.indexes_values {α : Type u_1} (p : α Prop) (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
def list.indexes_of {α : Type u_1} [decidable_eq α] (a : α) :
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
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
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
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
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
• = as
def list.mmap_with_index'_aux {m : Type v Type w} [applicative m] {α : Type u_1} (f : α ) :

Auxiliary definition for `mmap_with_index'`.

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

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

Equations
def list.lookmap {α : Type u_1} (f : α ) :
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
• (a :: l) = list.lookmap._match_1 a l l) (f a)
• 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
def list.countp {α : Type u_1} (p : α Prop)  :

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

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

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

Equations
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
Instances for `list.is_prefix`
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
Instances for `list.is_suffix`
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
Instances for `list.is_infix`
@[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
@[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
def list.sublists'_aux {α : Type u_1} {β : Type u_2} :
list α (list α list β) list (list β) list (list β)
Equations
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
def list.sublists_aux {α : Type u_1} {β : Type u_2} :
list α (list α list β list β) list β
Equations
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
def list.sublists_aux₁ {α : Type u_1} {β : Type u_2} :
list α (list α list β) list β
Equations
inductive list.forall₂ {α : Type u_1} {β : Type u_2} (R : α β Prop) :
list α list β Prop

`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.

@[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
Instances for `list.all₂`
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
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
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
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
• r (y :: ys) f = list.permutations_aux2._match_1 t y f r ys (λ (x : list α), f (y :: x)))
• f = (ts, r)
• list.permutations_aux2._match_1 t y f (us, zs) = (y :: us, f (t :: y :: us) :: zs)
def list.permutations_aux.rec {α : Type u_1} {C : list α list α Sort v} (H0 : Π (is : list α), 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
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
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
@[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
@[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
def list.erasep {α : Type u_1} (p : α Prop)  :
list α list α

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

Equations
def list.extractp {α : Type u_1} (p : α Prop)  :
list α × 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
• (a :: l) = ite (p a) , l) (list.extractp._match_1 a l))
• = , list.nil α)
• list.extractp._match_1 a (a', l') = (a', a :: l')
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
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
@[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
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
• h l = _ (f m, h⟩ :: l)
• h l = l
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
def list.of_fn_nth_val {α : Type u_1} {n : } (f : fin n α) (i : ) :

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

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

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

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

`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`
@[simp]
theorem list.pairwise_cons {α : Type u_1} {R : α α Prop} {a : α} {l : list α} :
(a :: l) ( (a' : α), a' l R a a')
@[protected, instance]
def list.decidable_pairwise {α : Type u_1} {R : α α Prop} (l : list α) :
Equations
def list.pw_filter {α : Type u_1} (R : α α Prop)  :
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
inductive list.chain {α : Type u_1} (R : α α Prop) :
α list α Prop

`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`
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
• (a :: l) = a l
Instances for `list.chain'`
@[simp]
theorem list.chain_cons {α : Type u_1} {R : α α Prop} {a b : α} {l : list α} :
a (b :: l) R a b b l
@[protected, instance]
def list.decidable_chain {α : Type u_1} {R : α α Prop} (a : α) (l : list α) :
Equations
• = list.rec (λ (a : α), (λ (l_hd : α) (l_tl : list α) (l_ih : Π (a : α), decidable a l_tl)) (a : α), l a
@[protected, instance]
def list.decidable_chain' {α : Type u_1} {R : α α Prop} (l : list α) :
Equations
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
Instances for `list.nodup`
@[protected, instance]
def list.nodup_decidable {α : Type u_1} [decidable_eq α] (l : list α) :
Equations
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
def list.destutter' {α : Type u_1} (R : α α Prop)  :
α 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
def list.destutter {α : Type u_1} (R : α α Prop)  :
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
@[simp]
def list.range'  :

`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
def list.reduce_option {α : Type u_1} :

Drop `none`s from a list, and replace each remaining `some a` with `a`.

Equations
@[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
@[simp]
def list.last' {α : Type u_1} :
list α

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

Equations
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
def list.rotate' {α : Type u_1} :

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

Equations
def list.choose_x {α : Type u_1} (p : α Prop) (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
• (l :: ls) hp = dite (p l) (λ (pl : p l), l, _⟩) (λ (pl : ¬p l), list.choose_x._match_2 p l ls ls _))
• = _.elim
• list.choose_x._match_2 p l ls a, _⟩ = a, _⟩
def list.choose {α : Type u_1} (p : α Prop) (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
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
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
def list.mmap'_diag {m : Type Type u_1} [monad m] {α : Type u_2} (f : α α 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
@[protected]
def list.traverse {F : Type u Type v} [applicative F] {α : Type u_1} {β : Type u} (f : α F β) :
list α F (list β)
Equations
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
def list.slice {α : Type u_1} :

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

Equations
• m (x :: xs) = x :: m xs
• n xs = xs
@[simp]
def list.map₂_left' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α γ) :
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
def list.map₂_right' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β γ) (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
• as bs = bs as
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
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
@[simp]
def list.map₂_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α γ) :
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
def list.map₂_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β γ) (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
• as bs = bs as
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
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
def list.all_some {α : Type u_1} :

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
def list.fill_nones {α : Type u_1} :
list (option α) list α list α

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

``````fill_nones [none, some 1, none, none] [2, 3] = [2, 1, 3]
``````
Equations
def list.take_list {α : Type u_1} :
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) xs)
• = (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)
def list.to_rbmap {α : Type u_1} :
list α

`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
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
• (x :: xs) (i + 1) = list.to_chunks_aux._match_2 x xs i)
• (x :: xs) 0 = list.to_chunks_aux._match_1 x xs n)
• = (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)
def list.to_chunks {α : Type u_1} :

`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
meta def list.map_async_chunked {α : Type u_1} {β : Type u_2} (f : α β) (xs : list α) (chunk_size : := 1024) :
list β

Asynchronous version of `list.map`.

We add some n-ary versions of `list.zip_with` for functions with more than two arguments. These can also be written in terms of `list.zip` or `list.zip_with`. For example, `zip_with3 f xs ys zs` could also be written as `zip_with id (zip_with f xs ys) zs` or as `(zip xs \$ zip ys zs).map \$ λ ⟨x, y, z⟩, f x y z`.

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
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
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
def list.replace_if {α : Type u_1} :
list α 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
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
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
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