How to write symbols in VS code for a lean file?

Stream: new members

[Quantum_fluctuations]

I am sorry if this is very dumb question. But how do I type different mathematical symbols like "for all" symbol or "greater than or equal to" symbol in a VS code file for LEAN?

[Jeremy Tan]

Special characters can be entered by typing \ followed by their ASCII equivalent

[Jeremy Tan]

so the forall symbol is \forall, for example

[Jeremy Tan]

and the greater-than-or-equal-to sign is \>= (once you type the last character it automatically shows up)

[Kevin Buzzard]

greater-than-or-equal-to tends to avoided in mathlib by the way, because allowing its use doubles the number of inequality lemmas we have. \le (like in LaTeX) generates unicode <=.

A way of answering this question yourself is by finding some lean code which already exists with the symbol in, and hovering over the symbol you want to know the shortcut for.

[Filippo A. E. Nuccio]

Just to make Kevin's answer explicit, here are two snippets showing you how to sort out the way to write the "bot" symbol or the "Principal filter" in case you find them in some file:
princ.png bot.png

[MohanadAhmed]

You might find this list of unicode characters useful https://docs.julialang.org/en/v1/manual/unicode-input/. I find it very useful

[MohanadAhmed]

although the list is for julia REPL, all the ones I have tried in VS code so far have worked

[Patrick Massot]

There is no need to guess anything from an unrelated language, you can read https://github.com/leanprover/vscode-lean/blob/master/src/abbreviation/abbreviations.json