typing special characters

Stream: new members

[Joshua Coleman]

Hello everyone. I keep trying to learn lean, but every book that I read sort of skips the part that some of the keys they use don't exist on my keyboard (logical not, for example). Is there a resource that will tell me which keys to press to make the logic work?

[Joshua Coleman]

Hello everyone. I keep trying to learn lean, but every book that I read sort of skips the part that some of the keys they use don't exist on my keyboard (logical not, for example). Is there a resource that will tell me which keys to press to make the logic work?

[Mario Carneiro]

@Joshua Coleman hover over them in vscode and it will say how to input them

[Kyle Miller]

There's also the data file of all the abbreviations used by the VS Code extension: https://github.com/leanprover/vscode-lean4/blob/master/vscode-lean4/src/abbreviation/abbreviations.json

[Michael Stoll]

...which is also available in VSCode in the Lean ( ) menu under "Documentation -> Docview: Show All Abbreviations".

[Patrick Massot]

Joshua Coleman said:

Hello everyone. I keep trying to learn lean, but every book that I read sort of skips the part that some of the keys they use don't exist on my keyboard (logical not, for example). Is there a resource that will tell me which keys to press to make the logic work?

Which book are you reading? I just checked that #tpil, #mil and #fpil all discuss this topic very early on.

[Dan Grigsby]

Expanding (possibly needlessly) @Mario Carneiro 's "hover" tip, to enter characters in VSCode, type backslash (\) followed by an abbreviation. From my limited experience, things feel pretty consistent. \le is less than or equal, so \ge naturally follows.