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
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):
extends does not record
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: May 10 2021 at 18:22 UTC