Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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