The ancestor attributes is used to record the names of structures which appear in the
extends clause of a structure or class declared with old_structure_cmd set to true.
As an example:
set_option old_structure_cmd true
structure base_one := (one : ℕ)
structure base_two (α : Type*) := (two : ℕ)
@[ancestor base_one base_two]
structure bar extends base_one, base_two α
The list of ancestors should be in the order they appear in the extends clause, and should
contain only the names of the ancestor structures, without any arguments.
Returns the parents of a structure added via the ancestor attribute.
On failure, the empty list is returned.
Returns the parents of a structure added via the ancestor attribute, as well as subobjects.
Returns the (transitive) ancestors of a structure added via the ancestor
attribute (or reachable via subobjects).