Menu
I'm using Lean in VS Code under macOS Catalina with a U.S. keyboard. How do I enter symbols such as for the implication arrow, union, intersection, subset?
Is there some built-in or add-on palette to facilitate this? Or do I have to use Option key combinations and, if so, where do I find the appropriate codes?
614
Assuming you have installed Lean and Visual Studio Code, you can add the Lean extension to VSCode by clicking the extension icon in the view bar at left and searching for lean . Once you have installed the extension, clicking on lean in the extensions panel provides additional information.
To add cursors at arbitrary positions, select a position with your mouse and use Alt+Click (Option+Click on macOS). You can add additional cursors to all occurrences of the current selection with Ctrl+Shift+L. Note: You can also change the modifier to Ctrl/Cmd for applying multiple cursors with the editor.
From the Lean reference:
You can enter Unicode characters with a backslash. For example,
\ainserts anα.
Here are some ways to get the symbol codes:
Guess. Many of the symbols have intuitive names, like \union or \cup for ⋃.
Use the tooltip. If you already have the symbol, then hovering over it will reveal the code.
If all else fails, check translations.json. You can usually get away with guessing, though.
159
⟶ System preferences
⟶ Keyboard
⟶ Input Sources Tab
⟶ + at bottom left
⟶ add and select Unicode Hex Input
from panel on right
⟶ enter unicode characters via alt+[code]
⟶ example, to enter the sign for union, hold down Alt and press 222a
To find additional codes, you can simply Google search Unicode Union for example, and it's almost always the first hit
https://www.google.com/search?q=unicode+Union&oq=unicode+Union&aqs=chrome..69i57.3027j0j7&sourceid=chrome-mobile&ie=UTF-8
40
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
