Attributes on constructors

Stream: lean4

[Matthew Toohey]

Hello! I was wondering if there's any technical reason attributes can't appear on constructors. It's currently not implemented, and results in an error.

I have some use-cases that this it would be handy for (i.e. customizing the behaviour of other attributes and/or deriving implementations). Also for a more general application, I've noticed this sort of thing pop up a couple times, where a common attribute such as refl is applicable to a constructor, but has to be included outside the definition. It would be much nicer if you could write:

inductive ReflTransGen (r : α → α → Prop) (a : α) : α → Prop
  | @[refl] refl : ReflTransGen r a a
  | tail {b c} : ReflTransGen r a b → r b c → ReflTransGen r a c

...which currently parses, but then triggers the error above.

If there's no reason this wouldn't be possible, and others agree that it would be useful to have, I'd be happy to spend some time on implementing it. Thanks!

[Eric Wieser]

You can always write attribute [refl] ReflTransGen.refl after the inductive is over

[Eric Wieser]

But indeed it would be nice to support the syntax

[Eric Wieser]

An even simpler ask would be to have the error message inform the user of the attribute syntax in the meantime

[Notification Bot]

This topic was moved here from #general > Attributes on constructors by Eric Wieser.

[Matthew Toohey]

Eric Wieser said:

You can always write attribute [refl] ReflTransGen.refl after the inductive is over

Oh that's true, I guess I could at least make my stuff work by doing that for now.

[Kenny Lau]

I thought you already knew that, since you said:

Matthew Toohey said:

has to be included outside the definition

[Matthew Toohey]

Lol I should've after bringing up the ReflTransGen example but I didn't really process that it'd work for my use-cases

[Matthew Toohey]

That being said, it would still be much more convenient to be able to write these inline since I may need a lot of them, so if anyone who's familiar with the code could offer an opinion about whether this would be feasible, that'd be great!

[Kyle Miller]

This might be reasonable. I don't see anything in the Lean 4 issue tracker for this — could you try searching it again, and create an issue if there's nothing relevant?

Please include some motivating use cases. It would be helpful to have comparison to using attribute. The tough thing right now with the suggestion is that there's a reasonable workaround.

It'd be helpful to have some examples of mutual inductive types with some constructor attributes that help decide what order attributes ought to be applied. I'm imagining that the order would be (1) afterTypechecking attributes for all the inductive types in the block, then (2) those for all the constructors, then (3) afterCompilation attributes for all inductive types, and lastly (4) those for all constructors. Though maybe there are examples where (3) should come before (2)?

[Eric Wieser]

Perhaps

structure Foo where
  -- Invalid attribute: Attributes cannot be added to fields
  @[instance] [y : Fact True]

belongs in the same tracking issue

[Kyle Miller]

I'd suggest a different issue for that, but link them for sure.

[Matthew Toohey]

I've created an issue for this here: https://github.com/leanprover/lean4/issues/10521