ConditionallyCompleteLinearOrderBot.toOrderBot

Stream: mathlib4

[Violeta Hernández]

Is there a reason why docs#ConditionallyCompleteLinearOrderBot extends docs#Bot and has a field bot_le, instead of simply extending docs#OrderBot?

[Eric Wieser]

This is probably inherited from Lean 3 where the inheritance you want was probably not supported

[Eric Wieser]

You could try changing it and see what the benchmark says

[Violeta Hernández]

I'll test that in #17524

[Kevin Buzzard]

(remark: in another thread someone else was also claiming that the speedcenter was down).