mathlib3port [reassoc.1]

Stream: mathlib4

[Kevin Buzzard]

The autoporter generated attribute [reassoc.1] here which didn't work. In mathlib3 here it's just reassoc. I changed it back to reassocin mathlib4 and it works. Is this a bug in mathlib3port?

[Kevin Buzzard]

Same question. attribute [simp, reassoc] is being changed by the autoporter to attribute [simp, reassoc.1] which gives the error expected ']'. Do I just change it back to [simp, reassoc]? This is in !4#3939 .

[Kyle Miller]

That's weird that it does reassoc.1, but maybe it's a Good Thing because [simp, reassoc] should now be attribute [reassoc (attr := simp)].

[Kyle Miller]

The attr configuration tells it to apply the given attribute(s) to the current definition and the reassociated definition

[Kyle Miller]

It looks like there's a handful of [simp, reassoc] and [simp, elementwise] in the library that should be fixed.

[Kevin Buzzard]

Oh, if you think it's weird then perhaps I should do a better job of reporting it: the observation is that this line in mathlib3 becomes this line in mathlib3port.