Zulip Chat Archive

Stream: general

Topic: Two questions about VisualStudioCode

Antoine Chambert-Loir (Oct 28 2021 at 17:42):

I have two questions about Visual Studio Code and Unicode characters (I am on MacOS, version 1.61.2).

  1. How can one get the list of shortcuts, those that turn \alpha to α, etc. ?
  2. Some Unicode characters are not rendered correctly (such as the the letter with code 0x2098 in partial_sups : (ℕ → α) → ℕ →ₘ α). Do you understand why? how to remedy that?

Johan Commelin (Oct 28 2021 at 17:44):

1: https://github.com/leanprover/vscode-lean/blob/master/src/abbreviation/abbreviations.json

Johan Commelin (Oct 28 2021 at 17:45):

2: Which font are you using? Adobe Source Code Pro seems to be a popular choice with good unicode coverage.

Bryan Gin-ge Chen (Oct 28 2021 at 17:45):

There are some suggested fonts in the vscode-lean README file: https://github.com/leanprover/vscode-lean#other-potentially-helpful-settings

Bryan Gin-ge Chen (Oct 28 2021 at 17:46):

(I'm on macOS and those fonts have been sufficient for me)

Last updated: Dec 20 2023 at 11:08 UTC