Zulip Chat Archive
Stream: new members
Topic: how to type ‹
David Chanin (he) (S2'21) (Mar 07 2022 at 20:03):
How can I enter the "‹" character in lean? I see it in tutorials but I can't find any way to type it besides finding it somewhere and copy/pasting it. is there an escape sequence to enter it?
Julian Berman (Mar 07 2022 at 20:03):
\f< will do it
Julian Berman (Mar 07 2022 at 20:04):
(the f Is I believe for "French")
Julian Berman (Mar 07 2022 at 20:04):
Your editor can also answer this for you in general which is good to know about
Julian Berman (Mar 07 2022 at 20:04):
(One second and I'll remind myself how VSCode does so)
Arthur Paulino (Mar 07 2022 at 20:04):
Yeah, try hovering the symbol
Julian Berman (Mar 07 2022 at 20:04):
Aha ^ Thanks Arthur.
David Chanin (he) (S2'21) (Mar 07 2022 at 20:08):
Oh yeah, that works! And the hover is super useful too, I didn't realize that. Thank you so much!!
Riccardo Brasca (Mar 07 2022 at 20:09):
You can also bookmark this page
Bryan Gin-ge Chen (Mar 07 2022 at 20:09):
Note that in VS Code you can type a balanced pair with \f<> (there are similar shortcuts for several other bracket-like symbols).
David Chanin (he) (S2'21) (Mar 07 2022 at 20:14):
That's good to know!
Antoine Chambert-Loir (Mar 07 2022 at 22:15):
Riccardo Brasca said:
You can also bookmark this page
That page (and hover) both suggest that I can type a big summation sign by entering \Sum.
However, it only works when I type '\Sigma'.
Riccardo Brasca (Mar 07 2022 at 22:30):
That works for me :thinking:
Julian Berman (Mar 07 2022 at 22:33):
I don't see that (it saying \Sum works). I see \sum there, but that's it. Am I missing it?
Julian Berman (Mar 07 2022 at 22:34):
\S works though for me.
Riccardo Brasca (Mar 07 2022 at 22:34):
Ah yes, it's sum that works for me
Julian Berman (Mar 07 2022 at 22:35):
If I read correctly \sum is the only way to get the big operator one.
Last updated: Dec 20 2023 at 11:08 UTC