visual-studio-code - 如何在 VS Code for Lean (macOS) 中输入符号

Question

我在 macOS Catalina 下使用美国键盘在 VS Code 中使用 Lean。如何输入符号，例如暗示箭头、联合、交集、子集？

是否有一些内置或附加调色板来促进这一点？或者我是否必须使用 Option 键组合，如果是这样，我在哪里可以找到合适的代码？

Answer 1

来自 Lean reference :

You can enter Unicode characters with a backslash. For example, \a inserts an α.

以下是获取符号代码的一些方法:

猜测。 许多符号都有直观的名称，例如 \union或 \cup为 ⋃ .

使用工具提示。 如果您已经拥有该符号，则将鼠标悬停在该符号上将显示代码。

如果您没有符号，右键单击 > 转到相关符号的定义通常会让您靠近。

如果所有其他方法都失败，请检查 translations.json .不过，您通常可以避免猜测。