English
Let f be a function of type Option α → β → γ. For lists as and bs, map₂Right' f as bs returns the pair (gs, as_remaining) where gs is obtained by applying f to each pair (Some a_i, b_i) for i up to the length of bs, and for any remaining b_i (when as is exhausted) f is applied to None. The second component is the list of elements of as that were not used in pairing. In particular, map₂Right' prod.mk [1] ['a','b'] = ([(some 1, 'a'), (none, 'b')], []) and map₂Right' prod.mk [1, 2] ['a'] = ([(some 1, 'a')], [2]).
Русский
Пусть f : Option α → β → γ. Для списков as и bs функция map₂Right' f as bs возвращает пару (gs, tail), где gs получается путём применения f к каждой паре (Some a_i, b_i) для i до длины bs, а для оставшихся элементов bs применяется f(None, b_i) при отсутствии a_i. Второй компонентом является остаток списка as, который не успели использовать. Например, map₂Right' prod.mk [1] ['a','b'] = ([(some 1, 'a'), (none, 'b')], []) и map₂Right' prod.mk [1, 2] ['a'] = ([(some 1, 'a')], [2]).
LaTeX
$$$$\text{mapAccum2Right}'(f)(a_s)(b_s) = (g_s, a_s\setminus b_s) \,,$$$$
Lean4
/-- 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])
```
-/
def map₂Right' (f : Option α → β → γ) (as : List α) (bs : List β) : List γ × List α :=
map₂Left' (flip f) bs as
