RFC: Support attribute declaration modifiers on inductive constructors

[mtoohey31]

Proposal

We should support attribute declaration modifiers on inductive constructors. This would allow the following example from mathlib here:

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

attribute [refl] ReflTransGen.refl

...and many similar examples to be simplified to something like this:

@[mk_iff ReflTransGen.cases_tail_iff]
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

Though it does work, I think using the attribute command afterwards isn't ideal as it may be missed by anyone reading the type's declaration, especially if there are any commands separating it from the original definition for one reason or another (i.e. a mutual block).

As another example, I'm working on making a library which automatically generates type class instances for substitutions (for programming language syntax definitions). For something like lambda calculus, I'd like to be able to define it as:

inductive Lambda where
  | @[var] var (x : Nat)
  | @[bind x in e] lam (x : Nat) (e : Lambda)
  | app (e₀ e₁ : Lambda)
deriving Subst

This way, similarly to the example above, the reader immediately sees how bindings are defined while reading the structure. Though it's not too bad to have to use attribute below for a short example like this, in practical uses I would expect syntax definitions with 10+ constructors to be common, in which case jumping back and forth between the constructor itself, and the things specified in the attribute will become annoying.

It seems like this shouldn't be too difficult to support, since it probably just involves calling the existing machinery for running attributes from the inductive elaboration code. One open question raised by Kyle Miller here is what order things should be processed in. I'm inclined to agree with his ordering; I believe that would work for all the examples I've considered.

I would be happy to spend some time doing the implementation if there is support for this change.

Community Feedback

I found one prior inquiry about this here, and then there's my own thread here. In both of these threads, people ask whether this is supported, and are disappointed it isn't.

Impact

Add :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.