如何在 VS Code for Lean (macOS) 中输入符号

Question

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

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

Answer 1

来自精益参考：

\n

\n

您可以输入带有反斜杠的 Unicode 字符。例如，\\a插入一个\xce\xb1.

\n

\n

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

\n

\n

• 猜测。许多符号都有直观的名称，例如\\union或\\cupfor\xe2\x8b\x83。

  \n
\n

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

  \n
  \n
  • 如果您没有该符号，右键单击 >转到相关符号的定义通常会很方便。
  \n
  \n
\n

• 如果所有其他方法均失败，请检查translations.json. 不过，你通常可以不用猜测。

  \n
\n

\n