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

Split a list at every element satisfying a predicate.

Equations
def list.split_on {α : Type u} [decidable_eq α] :
α → 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 α] :
list α → α

"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} :
(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} :
(α → α)list αlist α

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

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

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

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

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

Equations
def list.insert_nth {α : Type u} :
α → 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 α] :
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} :
(α → β → α)α → 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} :
(α → β → β)β → 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} :
(α → β → β)β → 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} :
(α → β γ)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] :
(α → 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} :
(α → 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} :
(α → m bool)list αm (option α)

A variant of mbfind' with more restrictive universe levels.

Equations
def list.many {m : Type → Type v} [monad m] {α : Type u} :
(α → 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} :
(α → m bool)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
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} :
(α → β → α)α → list β → α

Auxiliary definition for foldl_with_index.

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

Auxiliary definition for foldr_with_index.

Equations
def list.foldr_with_index {α : Type u} {β : Type v} :
(α → β → β)β → 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] :
list α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] :
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 α] :
α → 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} :
(β → α → m β)β → 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} :
(α → β → m β)β → 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} :
(α → 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} :
(α → m β)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} :
(α → 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} :
(α → m punit)list αm punit

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

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

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

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

erase p l removes all elements 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} :
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} :
list α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} :
list α(Π (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 : } :
(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 : } :
(fin n → α)option α

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

Equations
def list.disjoint {α : Type u} :
list αlist α → Prop

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

Equations
inductive list.pairwise {α : Type u} :
(α → α → 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} :
(α → α → 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} :
(α → α → 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} :
list α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 α) :
(∃ (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 α) :
(∃ (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} :
(α → 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} :
(α → α → 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} :
(α → α → 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 β)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} :
(α → 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} :
(option αβ → γ)list α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} :
(α → 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} :
(option αβ → γ)list α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