EReal.toReal.toEReal

Stream: mathlib4

[Martin Dvořák]

We mix three different notations in immediate succession:

https://github.com/leanprover-community/mathlib4/blob/fba419c6646ecec8022c9edaf0f22bab4ae5473b/Mathlib/Data/Real/EReal.lean#L411
(x.toReal : EReal)

https://github.com/leanprover-community/mathlib4/blob/fba419c6646ecec8022c9edaf0f22bab4ae5473b/Mathlib/Data/Real/EReal.lean#L416
x.toReal where .toEReal is left out

https://github.com/leanprover-community/mathlib4/blob/fba419c6646ecec8022c9edaf0f22bab4ae5473b/Mathlib/Data/Real/EReal.lean#L422
↑x.toReal

Furthermore, it is possible to write x.toReal.toEReal explicitly.
Which notation should we use?

[Eric Wieser]

These all mean the same thing to lean, don't they?

[Martin Dvořák]

Yes. I claim we shouldn't mix these notations in the same file, at least when they are used in similar contexts.

[Martin Dvořák]

Which notation is desirable here?

[Eric Wieser]

All that really matters is what ends up in the theorem statement, and here you get the same thing whichever spelling you pick

[Kevin Buzzard]

Right, they're all syntactically equal once they've been elaborated as terms of EReal.

[Martin Dvořák]

Am I the only one who cares what the code looks like?
Why don't we stick to one spelling, at least in these two statements that are symmetrical?
https://github.com/leanprover-community/mathlib4/blob/fba419c6646ecec8022c9edaf0f22bab4ae5473b/Mathlib/Data/Real/EReal.lean#L416
https://github.com/leanprover-community/mathlib4/blob/fba419c6646ecec8022c9edaf0f22bab4ae5473b/Mathlib/Data/Real/EReal.lean#L422

[Edward van de Meent]

my guess would be that the second example is the way it is because lean infers the coersion by itself due to the lhs being EReal, meaning less typing. this trick doesn't work for example 1 or 3, however... or at least, i don't think it does...

[Edward van de Meent]

if we were to pick any standard spelling for this, it can't be the second one

[Yaël Dillies]

I don't think it's worth spending energy on this

[Eric Wieser]

Indeed, the energy is better spent on fixing inconsistencies which _do_ end up in the final theorem statements

[Richard Osborn]

Lean pretty prints them all with the ↑ arrow. It would make most sense to follow that convention in the code, imo.

[Richard Osborn]

This also will have the code match how the documentation prints it.

[Ruben Van de Velde]

I think we should only write up-arrows in code in exceptional circumstances

[Kevin Buzzard]

My instinct is to write as little as possible. For example I'd explicitly coerce to EReal if lean doesn't see that this is what I want, but I would not do this if lean already knows that it's expecting an EReal. Hence what I write depends on context, and in particular I want the flexibility to be able to write what I want.