Mul match_pattern

Stream: lean4

[Marcus Rossel]

Why does the following work for Add but not Mul?

inductive E
  | add : E → E → E
  | mul : E → E → E

instance : Add E where
  add := .add

instance : Mul E where
  mul := .mul

def f : E → E
  | a + b => a
  | a * b => a -- invalid pattern, constructor or constant marked with '[match_pattern]' expected

[Eric Wieser]

I think it's there for Add to support n + 1 in matches

[Eric Wieser]

... and it has to be opted into explicitly, which I guess has not been done for Mul

[Marcus Rossel]

Eric Wieser said:

... and it has to be opted into explicitly, which I guess has not been done for Mul

Can I somehow opt in myself?

[François G. Dorais]

Attribute @[match_pattern]

[Kyle Miller]

Unfortunately it's a TagAttribute, so you can't add it from another module

[Marcus Rossel]

Kyle Miller said:

Unfortunately it's a TagAttribute, so you can't add it from another module

Too bad. Do you happen to know if this is just a temporary limitation, or is there a good reason for this?

[Kim Morrison]

This is for efficiency reasons. TagAttribute won't change in the near future.

[Mario Carneiro]

the usage of it for particular attributes might though

[Mario Carneiro]

although it seems like that approach is just going to lead to questions like "and why should we allow you to monkey patch our design decisions in this way?"

[Mario Carneiro]

at which point you may as well just propose the specific attribute you want placed upstream