zipWith

Stream: Is there code for X?

[Scott Morrison]

What is the closest we have to:

set_option autoImplicit true

@[simp] theorem zipWith_data {A : Array α} {B : Array β} {f : α → β → γ} :
    (Array.zipWith A B f).data = List.zipWith f A.data B.data := by
  sorry

Anything characterising Array.zipWith would be helpful!

[Martin Dvořák]

docs#Array.zipWith
There doesn't seem to be much.

[Eric Rodriguez]

@loogle Array.zipWith, List.zipWith

[loogle]

:shrug: nothing found

[Eric Rodriguez]

@loogle Array.zipWith

[loogle]

:shrug: nothing found

[Scott Morrison]

Yeah... :-) Sorry, I'd already got that far privately, should have specified.

[Eric Rodriguez]

Amazing news...

[Damiano Testa]

Whenever I see these attempts, I am always reminded of the old time and "let me Google that for you"!. With loogle, I would really welcome a "let me Loogle that for you!"