Как вводить символы в VS Code для Lean (macOS)

Question

Я использую Lean в VS Code под macOS Catalina с американской клавиатурой. Как ввести такие символы, как стрелка импликации, объединение, пересечение, подмножество?

Есть ли какая-нибудь встроенная или дополнительная палитра, чтобы облегчить это? Или я должен использовать сочетания клавиш Option и, если да, где мне найти соответствующие коды?

Answer 1

Из ссылки Lean :

Вы можете вводить символы Юникода с помощью обратного слэ sh. Например, \a вставляет α.

Вот несколько способов получить коды символов:

• Угадай. Многие символы имеют интуитивно понятные имена, например \union или \cup для ⋃.

• Используйте всплывающую подсказку. Если у вас уже есть символ , а затем наведя курсор на него, вы увидите код.

  • Если у вас нет символа, щелкните правой кнопкой мыши> Go до определения на связанном символе, и вы часто будете приземляться. рядом.

• Если ничего не помогло, проверьте translations.json. Обычно вы можете уйти от догадок.

Answer 2

⟶ Системные настройки
⟶ Клавиатура
⟶ Вкладка «Источники ввода»
⟶ + внизу слева
⟶ добавьте и выберите Unicode Hex Input
на панели справа
* введите символы Юникода в примере alt + [code]
,, чтобы ввести знак объединения, удерживайте Alt и нажмите 222a

Чтобы найти дополнительные коды, вы можете просто выполнить поиск Google Unicode Union например, и это почти всегда первый хит https://www.google.com/search?q=unicode+Union&oq=unicode+Union&aqs=chrome..69i57.3027j0j7&sourceid=chrome-mobile&ie=UTF-8