ancestor attribute

Stream: new members

[Yasmine Sharoda]

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.

[Nasos Evangelou-Oost]

(deleted)

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

(deleted)

[Eric Wieser]

There is an open github issue about documenting this

[Yury G. Kudryashov]

Clearly, PRs with better docs are welcome.

[Yasmine Sharoda]

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