How enter symbols in VS Code for Lean (macOS)

Question

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?

Answer 1

From the Lean reference:

You can enter Unicode characters with a backslash. For example, \a inserts 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 you don't have the symbol, right click > Go to definition on a related symbol will often land you close by.

• If all else fails, check translations.json. You can usually get away with guessing, though.

Answer 2

⟶ 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