English
Left-biased version of map₂: map₂Left' f as bs applies f to each pair (aᵢ, bᵢ) and, if bs runs out, applies f to (aᵢ, none) for remaining aᵢ, returning the results and the leftover bs.
Русский
Левая биасывающая версия map₂: map₂Left' f as bs применяет f к каждой паре (aᵢ, bᵢ) и, если bs кончается, применяет f к (aᵢ, none) для оставшихся aᵢ, возвращая результаты и оставшийся bs.
LaTeX
$$@[simp] def map₂Left' (f : \\alpha → Option β → γ) : List α → List β → List γ × List β\n | [], bs => ([], bs)\n | a :: as, [] => ((a :: as).map fun a => f a none, [])\n | a :: as, b :: bs =>\n let rec' := map₂Left' f as bs\n (f a (some b) :: rec'.fst, rec'.snd)$$
Lean4
/-- 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'])
```
-/
@[simp]
def map₂Left' (f : α → Option β → γ) : List α → List β → List γ × List β
| [], bs => ([], bs)
| a :: as, [] => ((a :: as).map fun a => f a none, [])
| a :: as, b :: bs =>
let rec' := map₂Left' f as bs
(f a (some b) :: rec'.fst, rec'.snd)
