mathlib4#588

Stream: mathlib4

[Jireh Loreaux]

Can someone review mathlib4#588? It's now at the top of the list of files which unlock the most stuff. I co-authored it with Anatole, so I shouldn't review it.

[Eric Rodriguez]

there's still a lot of ₓs in the #aligns - I thought this wasn't wanted?

[Jireh Loreaux]

I can add notes for these, but the first three are just orders of implicit arguments (actually the third one might also be that Seq.seq and has_seq.seq have different types, but this is known and expected). If you look at the translation error for Sum.bind it seems that mathport got it wrong, it shouldn't be dubious. If you want to look at the dubious translation errors, see commit: 41b163554e4c5dca5ea9e09b27ef475cafe61606

[Eric Rodriguez]

sorry, I'm still new to the porting process; so should these be left in if the aligns are still mildly dubious? I thought they were autogenerated by mathport and were meant to be all taken out before the file was "ported"

[Jireh Loreaux]

No, the purpose of the ₓ is to indicate that the type of the mathlib3 version and the mathlib4 version don't match. This is just a marker for mathport so that in future references to this declaration it knows to use the mathlib4 type. I don't think the ₓ is ever added automatically by mathport (I could be wrong here), it just suggest to the user to use it.

[Jireh Loreaux]

So, the ₓ should stay in when the translation is dubious, but it's good to indicate for future reference why it was marked as dubious (this requires human assessment).

[Eric Rodriguez]

I see! I think it'd be good to add the explanations in.

[Scott Morrison]

Yeah, I think that every \_x that gets left in should probably have a comment.

[Scott Morrison]

(and if mathport reports a dubious translation, but it actually looks okay, just remove the \_x.)

[Jireh Loreaux]

I had added comments, but I need to be done for the evening.