Zulip Chat Archive

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.

Nasos Evangelou-Oost (Feb 02 2021 at 03:51):


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.

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


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

Last updated: Dec 20 2023 at 11:08 UTC