Zulip Chat Archive
Stream: new members
Topic: VSCode monospaced font
Martin Dvořák (Jun 03 2022 at 08:52):
It is possible to set a monospaced font in VSCode? But most importantly, I need it to display all characters that are used in Lean. I work in the default settings and I hate how ⟨ is thinner than other characters.
Damiano Testa (Jun 03 2022 at 09:01):
If you dislike ⟨, then you may also dislike ⊹ and ₊... :upside_down:
Damiano Testa (Jun 03 2022 at 09:02):
Apart from the Amazon suggestions, though, I am not able to help, sorry!
Eric Taucher (Jun 03 2022 at 09:10):
There is a relatively new font that might be of benefit for what you seek which is free.
JetBrains is a company know for creating Integrated Development Environments (IDEs) for popular programming languages.
Mono refers to the fact that the font is a monospaced font meaning each glyph takes has the same width.
The only downside I have found with the font is that it is not a predefined option in the font list of many tools so the font has to be downloaded and installed. (instructions) Other than that it is one of my go to fonts now.
One interesting side note about JetBrains Mono, there is a WOFF (Web Open Font Format) version.
Last updated: Dec 20 2023 at 11:08 UTC