Zulip Chat Archive

Stream: general

Topic: Underscores and over scores


Kind Bubble (Jan 02 2023 at 17:29):

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

Σi=1nfi\Sigma_{i= 1}^n f_i

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

Martin Dvořák (Jan 02 2023 at 17:30):

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

Martin Dvořák (Jan 02 2023 at 17:31):

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

Heather Macbeth (Jan 02 2023 at 17:46):

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 (Jan 02 2023 at 18:04):

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 (Jan 02 2023 at 18:33):

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 (Jan 02 2023 at 18:33):

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 (Jan 02 2023 at 18:36):

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 (Jan 02 2023 at 18:39):

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

Eric Rodriguez (Jan 02 2023 at 18:39):

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

Niels Voss (Jan 02 2023 at 18:51):

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.


Last updated: Dec 20 2023 at 11:08 UTC