## Stream: new members

### Topic: ancestor attribute

#### Yasmine Sharoda (Feb 02 2021 at 02:38):

The definition of monoid in mathlib (described here) goes as follows:

@[ancestor semigroup has_one]
class monoid (M : Type u) extends semigroup M, has_one M :=
(one_mul : ∀ a : M, 1 * a = a) (mul_one : ∀ a : M, a * 1 = a)


Why do we need to define the ancestor attribute if we have the extends part?
It is uniformly used in the same file whenever extends is used.

(deleted)

#### Yury G. Kudryashov (Feb 02 2021 at 03:51):

Unfortunately, extends does not record semigroup and has_one in a way that can be used by metaprogramming.

(deleted)

#### Eric Wieser (Feb 02 2021 at 07:40):

There is an open github issue about documenting this

#### Yury G. Kudryashov (Feb 02 2021 at 19:53):

Clearly, PRs with better docs are welcome.

#### Yasmine Sharoda (Feb 02 2021 at 21:19):

Here is the issue, for reference
https://github.com/leanprover-community/mathlib/issues/5338

Last updated: May 10 2021 at 18:22 UTC