Underscores and over scores

Stream: general

[Kind Bubble]

Do you think there will be any interest in underscores and over scores like latex has? Minted has the "escape between" option. Unfortunately this makes the subsequent text italic for me and I can't figure out why. But anyways it would be nice to be able to type things like

$$\Sigma_{i= 1}^n f_i$$

I imagine something which is a bit more seamless with ordinary mathematical parlance this way.

[Martin Dvořák]

I don't think it would fit into a line.

[Martin Dvořák]

We like unicode because it combines advantages of both "looking like math" and "being a plain text".

[Heather Macbeth]

This is actually pretty frequently mentioned by mathematicians as on our wishlists, see e.g.

Kevin Buzzard said:

I can't wait for the day when someone figures out how to use latex instead, we get all the symbols we want and the computer scientists complain about yet another layer of obfuscation

But there are technical difficulties, e.g.

Gabriel Ebner said:

I think this would be problematic for at least our github workflow since we don't control the text display there

And also Zulip, email, git diff. The great thing about Unicode is that it works everywhere equally badly.

[Niels Voss]

Maybe a way to render LaTeX in the info panel on the right would be a compromise? That seems to be where we direct most of our attention when proving, but has the advantage that it isn't stored. I don't really know if this is possible

[Eric Wieser]

The danger with rendering things in LaTeX in this way is that it hides that the statement is actually a sum over a finite set rather than a more abstract sum over a sequence; information which is crucial when actually looking for the lemma to use

[Eric Wieser]

To some extent this could be resolved by the widget view showing the "real" lean code when you hover over it, but I suspect integrating widget hovers with MathJax / KaTeX output is hard for boring web reasons

[Eric Wieser]

Is Lean4's pretty-printing framework flexible enough to let us implement a LateX pretty-printer in an extensible way, without having to resort to raw constructor matching on exprs?

[Eric Rodriguez]

I was going to make a feature request to be able to use unicode sub/superscripts in parameters

[Eric Rodriguez]

but figuring out exactly how to do that and exactly how to implement it is likely tough

[Niels Voss]

Eric Wieser said:

The danger with rendering things in LaTeX in this way is that it hides that the statement is actually a sum over a finite set rather than a more abstract sum over a sequence; information which is crucial when actually looking for the lemma to use

Well it would probably have to be a button that would toggle LaTeX and normal mode. There are several reasons not to have LaTeX mode be the default, like what you said about it being hard to find lemmas.