oops

Stream: batteries

[Kim Morrison]

@Mario Carneiro, I foolishly slightly changed the statement of List.zipWith_map_left/rightwhile upstreaming them in std4#288, and have now fixed them in std4#296.

[Kim Morrison]

It would be good to fix this so I can proceed with the Mathlib bump.

[Mario Carneiro]

hm, this makes me slightly sad, I liked your revision

[Kim Morrison]

Ah, okay.

[Kim Morrison]

It does look like it is only one proof in Mathlib that breaks.

[Kim Morrison]

I can probably rewrite it.

[Mario Carneiro]

those compositions usually have to be simped away explicitly

[Kim Morrison]

In this case they somehow helped.

[Kim Morrison]

Some simp lemma liked the composition. I didn't stop to look too hard.

[Kim Morrison]

So... keep the new statement, or revert for the sake of not having to touch Mathlib?

[Kim Morrison]

I'm happy either way.

[Mario Carneiro]

I vote for keeping it

[Kim Morrison]

Okay! There is a simpa proof on branch#bump_std that is broken, and I'm not seeing how to ungolf it immediately. If anyone would like to look at it that would be lovely.

[Sébastien Gouëzel]

Done.