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