extending two extensions of a structure without redundancy

Stream: general

[Dean Young]

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

[Alistair Tucker]

According to Functional Programming in Lean (about Lean 4): "Structures may inherit from other structures. Behind the scenes, a structure that inherits from another structure contains an instance of the original structure as a field. In other words, inheritance is implemented with composition. When multiple inheritance is used, only the unique fields from the additional parent structures are used to avoid a diamond problem, and the functions that would normally extract the parent value are instead organized to construct one. Record dot notation takes structure inheritance into account."