What does attribute mean as body of a class definition

Stream: new members

[Lars Ericson]

It seems like attribute is the body of this class definition. Is that correct? If so, what does it do:

/-- An additive commutative monoid is an additive monoid with commutative `(+)`. -/
@[protect_proj, ancestor add_monoid add_comm_semigroup]
class add_comm_monoid (M : Type u) extends add_monoid M, add_comm_semigroup M
attribute [to_additive] comm_monoid

[Bryan Gin-ge Chen]

No, that's not correct. add_comm_monoid is simply a class that includes all the fields of add_monoid and add_comm_semigroup and nothing else.

[Bryan Gin-ge Chen]

attribute is a built-in command telling Lean to apply a certain attribute, in this case attr#to_additive, to a certain declaration, in this case comm_monoid. See the reference manual.

[Lars Ericson]

Thanks, it was just the formatting was confusing in this file. The use of white space gives a visual cue of relatedness to the prior declaration:

/-- A commutative additive semigroup is a type with an associative commutative `(+)`. -/
@[protect_proj, ancestor add_semigroup]
class add_comm_semigroup (G : Type u) extends add_semigroup G :=
(add_comm : ∀ a b : G, a + b = b + a)
attribute [to_additive] comm_semigroup

section comm_semigroup
variables {G : Type u} [comm_semigroup G]