Algebra.Free

Stream: mathlib4

[Lukas Miaskiwskyi]

Corresponding PR: mathlib4#1353

There are multiple interesting issues explained in this PR, maybe the first one is good to focus on: attribute [match_pattern] Mul.mul gives the error invalid attribute 'match_pattern', declaration is in an imported module .

I'm guessing this just means it's not happy that we are applying an attribute to Mul.mul which was declared in another file. In the mathlib3 version, the line attribute [pattern] has_mul.mul has no such error. How could one remedy this? And what does this attribute even achieve here?

[Yaël Dillies]

This attribute is to let you do matches on *, as in

match a with
| b * c => _
| _ => _

[Yaël Dillies]

This is useful for free stuff because ⟦[a]⟧ * ⟦l⟧ corresponds to a :: l.

[Eric Wieser]

I think you can just add the attribute in the file where docs4#Mul is defined

[Eric Wieser]

But you might find that the attribute actually needs to be on docs4#HMul

[Lukas Miaskiwskyi]

Alright, so I'm reading it correctly that in mathlib3, it retroactively applies the [matching] attribute to the mul functions of all has_mulinstances? Seems funky, but I will see whether adding it to Mul or HMul directly in mathlib4 breaks anything. Thanks for the explanations!

[Lukas Miaskiwskyi]

Realized that the Mul classes are defined in Init.Prelude, which seems like a pretty fundamental file. Is this really worth changing that file over, or can we finda a local solution? :)

[Xavier Roblot]

@Lukas Miaskiwskyi Thanks a lot for your help on this PR!