6

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?

murray
  • 737
  • 2
  • 10
  • 28

2 Answers2

5

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.

Lambda Fairy
  • 13,814
  • 7
  • 42
  • 68
  • 1
    You can also select and hover over a character to see how to insert it. – Christopher Hughes May 01 '20 at 03:24
  • Is there some VS Code plug-in that provides a palette for selecting those characters. (It seems very wasteful of screen space to have to have a separate window open with the translations.json page. – murray May 02 '20 at 15:58
  • @ChristopherHughes: Huh? Where do I find, say, a cap symbol (for set union) to hover over so as to discover what input to type to get it? – murray May 02 '20 at 16:03
  • If you're using anyone else's Lean code, this is a very handy tip. If you're using set union, then the symbol will be in the relevant library file. Alternatively paste it from somewhere else. – Christopher Hughes May 02 '20 at 20:18
  • You can always guess. Without viewing the list, I surmised that `\cap` would enter a set union symbol. And I was right. – Lambda Fairy May 02 '20 at 23:35
  • @murray I've expanded on how to find the symbol codes; hope this helps. From experience, I've never had to refer to `translations.json`; guessing and "go to definition" have been enough. – Lambda Fairy May 11 '20 at 11:01
  • The `translations.json` file has been moved [here](https://github.com/leanprover/vscode-lean/blob/master/src/abbreviation/abbreviations.json). – eyelash Jun 22 '21 at 22:57
1

⟶ 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

ultraGentle
  • 5,084
  • 1
  • 19
  • 45
  • That does not seem to be of use: after I added that input source and open the keyboard viewer for Unicode Hex Input, what I see looks like the ordinary English keyboard. How do I see keys to press for various symbols, such as the math symbol cap (for union)? – murray May 02 '20 at 16:01
  • Yes, the keyboard looks like English, but it now allows input of any unicode character. See edit above – ultraGentle May 02 '20 at 16:25
  • I use as part of my daily work flow for Greek letters, mathematical symbols, arrows, etc. Seems initially inconvenient, but you quickly build a repertoire of symbols, and then it is second nature and quite useful to have the actual characters available and in line – ultraGentle May 02 '20 at 16:33