Zulip Chat Archive

Stream: general

Topic: ancestor


view this post on Zulip Sebastien Gouezel (Aug 14 2020 at 17:40):

Can someone explain what the ancestor attribute is for? (It doesn't appear as an attribute in https://leanprover-community.github.io/mathlib_docs/attributes.html, and is only mentioned in to_additive there). For instance, I can see in field.lean

@[protect_proj, ancestor division_ring comm_ring]
class field (α : Type u) extends comm_ring α, has_inv α, nontrivial α :=
(mul_inv_cancel :  {a : α}, a  0  a * a⁻¹ = 1)
(inv_zero : (0 : α)⁻¹ = 0)

which mentions as ancestordivision_ring, but not has_inv or nontrivial, so I have a hard time guessing how it should be used in general.

view this post on Zulip Mario Carneiro (Aug 14 2020 at 17:42):

I think field's ancestry was changed

view this post on Zulip Mario Carneiro (Aug 14 2020 at 17:42):

it's supposed to list the contents of the extends clause, because this information is not preserved by old_structure_cmd structures

view this post on Zulip Sebastien Gouezel (Aug 14 2020 at 17:45):

ok, so in the case of field it should just be comm_ring has_inv nontrivial?

view this post on Zulip Sebastien Gouezel (Aug 14 2020 at 17:47):

And if you extend things with less params (for instance bar (a b) extends foo1 a, foo2 b), should it just be ancestor foo1 foo2 or is there some more trickery do be done?

view this post on Zulip Patrick Massot (Aug 14 2020 at 17:59):

I think this is used only by the subtype instance tactic which is maybe no longer used now everything is bundled.

view this post on Zulip Mario Carneiro (Aug 14 2020 at 18:09):

I think it is just ancestor foo1 foo2

view this post on Zulip Mario Carneiro (Aug 14 2020 at 18:10):

that said, you shouldn't be doing that in the first place

view this post on Zulip Kevin Buzzard (Aug 14 2020 at 18:16):

Sebastien Gouezel said:

And if you extend things with less params (for instance bar (a b) extends foo1 a, foo2 b), should it just be ancestor foo1 foo2 or is there some more trickery do be done?

Isn't this an antipattern?

view this post on Zulip Sebastien Gouezel (Aug 14 2020 at 18:55):

This is an antipattern for classes, as typeclass search will go crazy, but for normal structures it shouldn't be a problem.

view this post on Zulip Yury G. Kudryashov (Aug 15 2020 at 01:29):

ancestor is used by to_additive to automatically map to_* functions. I don't know who else uses this information.

view this post on Zulip Yury G. Kudryashov (Aug 15 2020 at 01:30):

In particular, I don't know if there is some code using @[ancestor] on field.

view this post on Zulip Floris van Doorn (Aug 15 2020 at 22:56):

Yury G. Kudryashov said:

ancestor is used by to_additive to automatically map to_* functions. I don't know who else uses this information.

Oh, I didn't know about the ancestor attribute. We could use this for the is_auto_generated definition to check which instances are auto-generated (which is useful for e.g. linters).

view this post on Zulip Eric Wieser (Feb 18 2021 at 18:00):

attr#ancestor and attr#to_additive now collectively document this i think


Last updated: May 14 2021 at 06:16 UTC