attributes on inductive constructors

Stream: lean4

[Jad Ghalayini]

I've been messing around with custom attributes, and was wondering if there was any support for attributes on the constructors of an inductive type. They seem to be accepted by the syntax, but throw an error on usage. The intended use is to indicate which constructor I'm talking about in an attribute on the inductive type and/or a custom derive without needing to repeat the constructor name; another example would, e.g., be to indicate the constructor to use for a "Default" trait like in Rust

[Alex Keizer]

@Jad Ghalayini, did you ever get the answer to this question?

I've also been toying around with attributes, and found out that adding the attributes post-hoc is accepted, as in:

inductive Foo
  | ctorA

attribute [extern "A"] Foo.ctorA

But, trying to define the attribute inline throws a "invalid use of attributes in constructor declaration" error:

inductive Foo
  | @[extern "A"] ctorA

I was hoping that error means that somehow the way I use the attributes is invalid, rather than attributes in constructor declarations always being invalid, but I don't really see how.

[Kyle Miller]

It means that it's always invalid to use attributes on constructor, I just checked.

I believe the only modifiers that are accepted are private and protected.

[Kyle Miller]

Potentially we could have attributes on constructors. Post-hoc attribute commands are the way to go for now though.

[Damien Carré]

(deleted)

[Alex Keizer]

Thanks for checking!