ancestor attributes is used to record the names of structures which appear in the
extends clause of a
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.