Zulip Chat Archive

Stream: mathlib4

Topic: Question on #9645

Jeremy Tan (Mar 20 2024 at 04:03):

After updating #9645 (review/merge, please!) I encountered a question: one rw doesn't work because the synthed instances don't line up, and the only way I can get around this is two ugly converts. Is there a simpler way?

Jeremy Tan (Mar 21 2024 at 04:24):

Hello?

Filippo A. E. Nuccio (Mar 22 2024 at 22:37):

Can you point out at where this rw is? found it.

Filippo A. E. Nuccio (Mar 22 2024 at 23:00):

I got rid of one convert, but I would expect that exact can close the goal. At any rate, it is now just one line.

Filippo A. E. Nuccio (Mar 22 2024 at 23:01):

Oh, it had been merged in the meanwhile, you could have marked the topic as resolved :smile:

Last updated: May 02 2025 at 03:31 UTC