to_additive and structures

Stream: general

[Yaël Dillies]

Is there any difference between

structure add_foo :=
(add_bla : add_type)

structure mul_foo :=
(mul_bla : mul_type)

attribute [to_additive] mul_foo

and

structure add_foo :=
(add_bla : add_type)

@[to_additive]
structure mul_foo :=
(mul_bla : mul_type)

and does it still hold if I add more stuff around like class, protect_proj, ancestor or an extends clause?

[Kyle Miller]

protect_proj, ancestor, and to_additive are all user attributes, and they get processed at the end (after everything to do with the structure is added to the environment).

The class keyword and extends clauses are processed during the definition phase, but the class attribute itself seems to be applied along with all the user attributes. I'm not sure in which order these attributes are all applied.

Your first code example guarantees that to_additive is applied last.

[Kyle Miller]

It looks like class is applied first and then any attributes you give yourself are added in order.

[Yaël Dillies]

That's what I would have expected. So technically the second version works just as well, right?

[Kyle Miller]

Yes, the two examples should do the same thing.