Stream: general

Topic: ancestor

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.

Mario Carneiro (Aug 14 2020 at 17:42):

I think field's ancestry was changed

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

Sebastien Gouezel (Aug 14 2020 at 17:45):

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

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?

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.

Mario Carneiro (Aug 14 2020 at 18:09):

I think it is just ancestor foo1 foo2

Mario Carneiro (Aug 14 2020 at 18:10):

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

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?

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.

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.

Yury G. Kudryashov (Aug 15 2020 at 01:30):

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

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).

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