invalid structure header

Stream: general

[Jonathan Whitehead]

Hi, everyone. I'm new to Lean. I was a novice Coq user but have recently decided to devote myself to lean since it feels more friendly to mathematicians. Anyways, I'm also new to Zulip so I'm not sure if this is the format for asking questions. So if it's not, surely an admin can help me make a correction.

I'm creating a class that extends classes x_1 and x_2. However, x_1 and x_2 both extend class z. Thus, they share a field.

I'm receiving an error message saying "Invalid 'structure' header" because one of the fields in x_1 was already declared by x_2.

Does Lean have some kind of mechanism that I can use to avoid this error message? I feel like Lean should be smart enough to know that
if I'm extending two classes, and they share a field that it should only be declared once.

[Thomas Browning]

set_option old_structure_cmd true might do the trick