Zulip Chat Archive

Stream: new members

Topic: ancestor attribute


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

view this post on Zulip Nasos Evangelou-Oost (Feb 02 2021 at 03:51):

(deleted)

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

view this post on Zulip Yury G. Kudryashov (Feb 02 2021 at 03:52):

(deleted)

view this post on Zulip Eric Wieser (Feb 02 2021 at 07:40):

There is an open github issue about documenting this

view this post on Zulip Yury G. Kudryashov (Feb 02 2021 at 19:53):

Clearly, PRs with better docs are welcome.

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