Zulip Chat Archive

Stream: std4

Topic: oops

Scott Morrison (Oct 15 2023 at 10:57):

@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.

Scott Morrison (Oct 15 2023 at 10:58):

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

Mario Carneiro (Oct 15 2023 at 10:58):

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

Scott Morrison (Oct 15 2023 at 10:58):

Ah, okay.

Scott Morrison (Oct 15 2023 at 10:58):

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

Scott Morrison (Oct 15 2023 at 10:59):

I can probably rewrite it.

Mario Carneiro (Oct 15 2023 at 10:59):

those compositions usually have to be simped away explicitly

Scott Morrison (Oct 15 2023 at 10:59):

In this case they somehow helped.

Scott Morrison (Oct 15 2023 at 10:59):

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

Scott Morrison (Oct 15 2023 at 11:01):

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

Scott Morrison (Oct 15 2023 at 11:01):

I'm happy either way.

Mario Carneiro (Oct 15 2023 at 11:04):

I vote for keeping it

Scott Morrison (Oct 15 2023 at 11:21):

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.

Sebastien Gouezel (Oct 15 2023 at 11:42):

Done.

Last updated: Dec 20 2023 at 11:08 UTC