Zulip Chat Archive

Stream: lean4

Topic: attributes on inductive constructors


Jad Ghalayini (Jan 31 2023 at 17:42):

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


Last updated: Dec 20 2023 at 11:08 UTC