Redundant inheritance

Stream: general

[Alice Laroche]

Is there a way to let a class by an extension of two class who are extensions of the same class :
Something like this :
A
| \
B C
| /
D

[Eric Wieser]

Yes, see for example src#monoid

[Eric Wieser]

Which uses set_option old_structure_cmd true

[Eric Wieser]

If you don't want to use that option, see src#mul_action_with_zero for an example

[Alice Laroche]

Hmm, i probably misunderstand or misread something because mul_action_with_zero only inherit from one class ?

[Kevin Buzzard]

mul_action_with_zero seems to say that the answer is "copy the fields manually". The thing about set_option old_structure_cmd true is that it makes structures which can be slow to use for some reason; old structures have been removed from Lean 4.

[Eric Wieser]

Yes, Kevin is correct; without old_structure_cmd, the answer is "you can't do it automatically", but also "you can do it manually by defining docs#mul_action_with_zero.to_smul_with_zero yourself".

[Kevin Buzzard]

mul_action_with_zero "extends from smul_with_zero" in the weak sense that it copies the fields manually. If the old structure command setting is set, then you can just extend like you would imagine, and it works.

[Alice Laroche]

I tried the settings but i got a don't know how to synthesize placeholder error

[Sebastien Gouezel]

#mwe?

[Alice Laroche]

I'm on it

[Alice Laroche]

Erfff, sorry, i saw a typo while reducing to a MWE...
for my defense, the typo was three line below where the error was showing

[Kevin Buzzard]

Yeah, sometimes I get into the habit of writing #exit directly after the bit where I'm totally confused to see if this helps :-)

[Alice Laroche]

I wonder why the functionality was disabled tho, there was a bad trade-off ?

[Johan Commelin]

It can have bad performance

[Kevin Buzzard]

For many years the mathematicians here just complained about how it was going to disappear, and then around a year ago we started getting bad slowdown when doing some stuff and it finally dawned on us why Leo hated it so much :-)

[Johan Commelin]

Try #print linear_ordered_field if you want to be scared

[Kevin Buzzard]

Here's a detailed explanation of why Leo wanted to switch: https://github.com/leanprover/lean/wiki/Refactoring-structures

[Kevin Buzzard]

In that message, "currently" := "old_structure_cmd", and "the new proposal" is the current default.

[Alice Laroche]

Okayyy, i can see the problem
Hope there will be a way one day because the new way of redundant inheritance is... well, it still can be usefull, but it loose usefullness

[Alice Laroche]

And is there a way to not add new field ?
Since i only wanted to unifies two different class.
(let's say, for exemple, i have the injective class and the surjective class and i want to create the bijective class)
It seem useless, but i need it for a software who use lean in backend

[Anne Baanen]

Yes, just end the line with a . after extends foo α, bar α β, no :=.

[Alice Laroche]

Oh well

[Anne Baanen]

(Usually a . to end a statement can be left out, in this case I think you need it to help the parser.)