## Stream: new members

### Topic: What does attribute mean as body of a class definition

#### Lars Ericson (Dec 11 2020 at 02:22):

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 (Dec 11 2020 at 02:36):

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 (Dec 11 2020 at 02:38):

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 (Dec 11 2020 at 02:43):

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]


Last updated: May 14 2021 at 04:22 UTC