Structure which extends two different structures

Stream: new members

[Dean Young]

Is it possible to make a structure which extends two different structures at once?

[Alex J. Best]

https://leanprover.github.io/theorem_proving_in_lean/structures_and_records.html#inheritance

[Dean Young]

If two structures extend a common substructure, then does their mutual extension know not to duplicate the items in the common substructure?

[Jireh Loreaux]

Yes

[Jireh Loreaux]

If those fields have the same names.

[Eric Wieser]

@Kind Bubble, have you considered just trying this and seeing what happens?

[Eric Wieser]

Lean will give you a much faster answer to "what does this code do" than zulip will.

[Jireh Loreaux]

To follow-up on Eric's point, they way you would check this is:

structure foo :=
(x : nat)
(y : nat)

structure bar :=
(y : nat)
(z : nat)

structure baz extends foo, bar

#print baz