mathlib documentation

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

def list.is_nil {α : Type u_1} :
list αbool

Returns whether a list is []. Returns a boolean even if l = [] is not decidable.

Equations
@[instance]
def list.has_sdiff {α : Type u} [decidable_eq α] :
Equations
def list.split_at {α : Type u} :
list αlist α × list α

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) [decidable_pred P] :
list α(list αlist α)list (list α)

An auxiliary function for split_on_p.

Equations
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
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} :
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} :
list αoption α

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

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

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

Equations
@[simp]
def list.inth {α : Type u} [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} (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
@[simp]
def list.modify_head {α : Type u} (f : α → α) :
list αlist α

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

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

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

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

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

Equations
def list.insert_nth {α : Type u} (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} [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} (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
def list.scanl {α : Type u} {β : Type v} (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
def list.scanr_aux {α : Type u} {β : Type v} (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
def list.scanr {α : Type u} {β : Type v} (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
def list.prod {α : Type u} [has_mul α] [has_one α] :
list α → α

Product of a list.

prod [a, b, c] = ((1 * a) * b) * c
Equations
def list.sum {α : Type u} [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} {β : Type v} {γ : Type w} (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} (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
def list.mfind {α : Type u} {m : Type uType 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
def list.mbfind' {m : Type uType 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
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) :
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
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] :
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
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
def list.foldl_with_index_aux {α : Type u} {β : Type v} (f : α → β → α) :
α → list β → α

Auxiliary definition for foldl_with_index.

Equations
def list.foldl_with_index {α : Type u} {β : Type v} (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
def list.foldr_with_index_aux {α : Type u} {β : Type v} (f : α → β → β) :
β → list α → β

Auxiliary definition for foldr_with_index.

Equations
def list.foldr_with_index {α : Type u} {β : Type v} (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
def list.find_indexes {α : Type u} (p : α → Prop) [decidable_pred p] (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} (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
def list.indexes_of {α : Type u} [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
def list.mfoldl_with_index {m : Type vType 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 vType 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 vType 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 vType w} [applicative m] {α : Type u_1} {β : Type v} (f : α → m β) (as : list α) :
m (list β)

Applicative variant of map_with_index.

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

Auxiliary definition for mmap_with_index'.

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

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

Equations
def list.lookmap {α : Type u} (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
def list.countp {α : Type u} (p : α → Prop) [decidable_pred p] :
list α

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

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

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

Equations
def list.is_prefix {α : Type u} (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
def list.is_suffix {α : Type u} (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
def list.is_infix {α : Type u} (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
@[simp]
def list.inits {α : Type u} :
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} :
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} {β : Type v} :
list α(list αlist β)list (list β)list (list β)
Equations
def list.sublists' {α : Type u} (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} {β : Type v} :
list α(list αlist βlist β)list β
Equations
def list.sublists {α : Type u} (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} {β : Type v} :
list α(list αlist β)list β
Equations
inductive list.forall₂ {α : Type u} {β : Type v} (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.

def list.transpose_aux {α : Type u} :
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} :
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} :
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} {β : Type v} (t : α) (ts : list α) (r : list β) :
list α(list α → β)list α × list β
Equations
def list.permutations_aux.rec {α : Type u} {C : list αlist αSort v} (H0 : Π (is : list α), C list.nil is) (H1 : Π (t : α) (ts is : list α), C ts (t :: is)C is list.nilC (t :: ts) is) (l₁ l₂ : list α) :
C l₁ l₂
Equations
def list.permutations_aux {α : Type u} :
list αlist αlist (list α)
Equations
def list.permutations {α : Type u} (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
def list.erasep {α : Type u} (p : α → Prop) [decidable_pred p] :
list αlist α

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

Equations
def list.extractp {α : Type u} (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
def list.revzip {α : Type u} (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} {β : Type v} (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
def list.sigma {α : Type u} {σ : α → Type u_1} (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} {n : } (f : fin n → α) (m : ) :
m nlist α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
def list.of_fn {α : Type u} {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} {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} (l₁ l₂ : list α) :
Prop

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

Equations
inductive list.pairwise {α : Type u} (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.

@[simp]
theorem list.pairwise_cons {α : Type u} {R : α → α → Prop} {a : α} {l : list α} :
list.pairwise R (a :: l) (∀ (a' : α), a' lR a a') list.pairwise R l
@[instance]
def list.decidable_pairwise {α : Type u} {R : α → α → Prop} [decidable_rel R] (l : list α) :
Equations
def list.pw_filter {α : Type u} (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. erase_dup), 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} (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
def list.chain' {α : Type u} (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
@[simp]
theorem list.chain_cons {α : Type u} {R : α → α → Prop} {a b : α} {l : list α} :
list.chain R a (b :: l) R a b list.chain R b l
@[instance]
def list.decidable_chain {α : Type u} {R : α → α → Prop} [decidable_rel R] (a : α) (l : list α) :
Equations
@[instance]
def list.decidable_chain' {α : Type u} {R : α → α → Prop} [decidable_rel R] (l : list α) :
Equations
def list.nodup {α : Type u} :
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
@[instance]
def list.nodup_decidable {α : Type u} [decidable_eq α] (l : list α) :
Equations
def list.erase_dup {α : Type u} [decidable_eq α] :
list αlist α

erase_dup l removes duplicates from l (taking only the first occurrence). Defined as pw_filter (≠).

erase_dup [1, 0, 2, 2, 1] = [0, 2, 1]
Equations
@[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
def list.reduce_option {α : Type u_1} :
list (option α)list α

Drop nones 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 αoption α

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

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

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

Equations
def list.choose_x {α : Type u} (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
def list.choose {α : Type u} (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
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 uType 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) :
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
def list.traverse {F : Type uType v} [applicative F] {α : Type u_1} {β : Type u} (f : α → F β) :
list αF (list β)
Equations
def list.get_rest {α : Type u} [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 αlist α

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

Equations
@[simp]
def list.map₂_left' {α : Type u} {β : Type v} {γ : Type w} (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
def list.map₂_right' {α : Type u} {β : Type v} {γ : Type w} (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
def list.zip_left' {α : Type u} {β : Type v} :
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} {β : Type v} :
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} {β : Type v} {γ : Type w} (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
def list.map₂_right {α : Type u} {β : Type v} {γ : Type w} (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
def list.zip_left {α : Type u} {β : Type v} :
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} {β : Type v} :
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} :
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
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
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
def list.to_rbmap {α : Type u} :

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

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

to_rb_map ['a', 'b', 'c'] = rb_map.of_list [(0, 'a'), (1, 'b'), (2, 'c')]
meta def list.to_chunks {α : Type u_1} (n : ) :
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.

TODO: make non-meta; currently doesn't terminate, e.g.

#eval [0].to_chunks 0
meta def list.map_async_chunked {α : Type u_1} {β : Type u_2} (f : α → β) (xs : list α) (chunk_size : := 1024) :
list β

Asynchronous version of list.map.