def List.zipWithAll {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : Option α → Option β → γ) : List α → List β → List γ

Version of List.zipWith that continues to the end of both lists, passing none to one argument once the shorter list has run out.

Equations

• List.zipWithAll f [] x = List.map (fun (b : β) => f none (some b)) x
• List.zipWithAll f (a :: as) [] = List.map (fun (a : α) => f (some a) none) (a :: as)
• List.zipWithAll f (a :: as) (b :: bs) = f (some a) (some b) :: List.zipWithAll f as bs

@[simp]

theorem List.zipWithAll_nil_right : ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : Option α → Option α_1 → α_2} {as : List α}, List.zipWithAll f as [] = List.map (fun (a : α) => f (some a) none) as

@[simp]

theorem List.zipWithAll_nil_left : ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : Option α → Option α_1 → α_2} {bs : List α_1}, List.zipWithAll f [] bs = List.map (fun (b : α_1) => f none (some b)) bs

@[simp]

theorem List.zipWithAll_cons_cons : ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : Option α → Option α_1 → α_2} {a : α} {as : List α} {b : α_1} {bs : List α_1}, List.zipWithAll f (a :: as) (b :: bs) = f (some a) (some b) :: List.zipWithAll f as bs