14
$\begingroup$

There was already a question here of this type but I would like to ask more generally:

If I see some strange unicode symbols being used in Lean, is there a recommended way to find out how to type them, and finding out what they mean, other than asking here at Proof Assistants or at the Zulip chat?

Is the best source the old Lean 2 Quick Reference from 2017?

$\endgroup$
2
  • $\begingroup$ +1. But I edited the last sentence to be emphasized in a different way, since the way you emphasized it is generally used for quotes, which doesn't seem to be what you were trying to do here. Also, would you be able to provide a hyperlink to the other question to which you referred here? I can guess which one it was, but it would probably be better if you do it! $\endgroup$ Feb 9, 2022 at 23:39
  • $\begingroup$ How to type them is mostly user/editor-specific; vscode and emacs are both highly customizable. But, how Lean recognizes unicode characters is all about Lean. It should be documented somewhere. Lean 2 was pretty well documented, I'm not sure about Lean 3 but I haven't looked recently. Lean 4 has a highly sophisticated macro system (with evolving lacunary documentation). With some mild to serious effort you can teach Lean 4 to interpret any symbol any way you want within a specific context. $\endgroup$ Feb 10, 2022 at 2:34

2 Answers 2

16
$\begingroup$

Unicode character input is an editor feature, so this answer is specific to VSCode.

If you have a Lean file open in VSCode, you can hover over a unicode symbol to see what input commands are available. E.g., if you paste the character • and put your cursor over it, you get the tooltip Type • using \smul or \bub or \bu. This works whether or not the character is used in syntactically correct form.

You can see a list of all the supported input abbreviations in the VSCode plugin.

$\endgroup$
3
6
$\begingroup$

If you are using Emacs, then the corresponding command is C-u C-x =. This displays a buffer with lots of information about the character under point, including its Unicode name and to input: which shows you how to type it in the current input-mode.

$\endgroup$
1
  • $\begingroup$ I can never remember that command, so I usually do M-x desc-ch (for describe-char). $\endgroup$ Feb 10, 2022 at 3:03

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.