Zulip Chat Archive
Stream: general
Topic: zip_with and map₂
Chris Hughes (Oct 13 2022 at 09:59):
At the moment we have two function on lists zip_with and map₂ that do the exact same thing, with lemmas proved about both of them. I guess we should get rid of one. Which one to get rid of?
Yaël Dillies (Oct 13 2022 at 10:00):
map₂ makes more sense as a name to me.
Scott Morrison (Oct 13 2022 at 10:17):
It is called zipWith in Std4.
Kevin Buzzard (Oct 13 2022 at 10:49):
What's map₂ called? ;-)
Patrick Johnson (Oct 13 2022 at 17:02):
Scott Morrison said:
It is called
zipWithinStd4.
It's also called zipWith in other languages, such as Haskell.
Reid Barton (Oct 13 2022 at 18:53):
As the name zip_with suggests, it is not analogous to docs#set.image2 (what could be the order of a set?)
Last updated: Dec 20 2023 at 11:08 UTC