zip & unzip #
This file provides results about List.zipWith
, List.zip
and List.unzip
(definitions are in
core Lean).
zipWith f l₁ l₂
applies f : α → β → γ
pointwise to a list l₁ : List α
and l₂ : List β
. It
applies, until one of the lists is exhausted. For example,
zipWith f [0, 1, 2] [6.28, 31] = [f 0 6.28, f 1 31]
.
zip
is zipWith
applied to Prod.mk
. For example,
zip [a₁, a₂] [b₁, b₂, b₃] = [(a₁, b₁), (a₂, b₂)]
.
unzip
undoes zip
. For example, unzip [(a₁, b₁), (a₂, b₂)] = ([a₁, a₂], [b₁, b₂])
.
@[deprecated List.getElem?_zipWith' (since := "2025-02-14")]
theorem
List.get?_zipWith'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{l₁ : List α}
{l₂ : List β}
{f : α → β → γ}
{i : ℕ}
:
Alias of List.getElem?_zipWith'
.
Variant of getElem?_zipWith
using Option.map
and Option.bind
rather than a match
.
@[deprecated List.getElem?_zipWith_eq_some (since := "2025-02-14")]
theorem
List.get?_zipWith_eq_some
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β → γ}
{l₁ : List α}
{l₂ : List β}
{z : γ}
{i : ℕ}
:
Alias of List.getElem?_zipWith_eq_some
.