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?

Improve this question
$\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$
    – Nike Dattani
    Commented 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$
    – François G. Dorais
    Commented Feb 10, 2022 at 2:34

2 Answers 2

Reset to default
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.

Improve this answer
$\endgroup$
3
  • $\begingroup$ In some ways, the official recommendation is that abbreviations.json file; it's copied over to all other editors. $\endgroup$
    – It'sNotALie.
    Commented Feb 9, 2022 at 23:52
  • $\begingroup$ Hmm I'll post it as a separate question you can answer, @It'sNotALie. $\endgroup$
    – Bjørn Kjos-Hanssen
    Commented Feb 10, 2022 at 0:35
  • $\begingroup$ proofassistants.stackexchange.com/q/237/65 $\endgroup$
    – Bjørn Kjos-Hanssen
    Commented Feb 10, 2022 at 0:40
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.

Improve this answer
$\endgroup$
1
  • $\begingroup$ I can never remember that command, so I usually do M-x desc-ch (for describe-char). $\endgroup$
    – Kyle Miller
    Commented 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.