====== Fonts ====== TLA+ widely uses the language of mathematics, and its syntax contains great deal of character sequences that represent mathematical symbols. So why not use those symbols directly when displaying specifications in the text editor? There’re two levels of visualization improvements: ===== Ligatures ===== Lots of fonts, especially designed for developers, have many ligatures that match TLA+ character sequences: [[https://github.com/tonsky/FiraCode|Fira Code]], [[https://larsenwork.com/monoid/|Monoid]], [[https://github.com/i-tu/Hasklig/|Hasklig]], [[https://www.jetbrains.com/lp/mono/|JetBrains Mono]], [[https://fsd.it/shop/fonts/pragmatapro/|PragmataPro]] to name a few. Switch to one of such fonts, turn ligatures on (provide the ''%%"editor.fontLigatures": true%%'' VS Code setting), and you’ll get many fancy symbols in your specs: {{https://github.com/alygin/vscode-tlaplus/blob/master/resources/images/fonts-ligatures.png|Fonts with ligatures}} Fonts with ligatures ===== Symbol substitutions ===== If you want go further, you can install the [[https://marketplace.visualstudio.com/items?itemName=BRBoer.vsc-conceal|Conceal extension]] and configure substitutions to make your specifications look even closer to math texts: {{https://github.com/alygin/vscode-tlaplus/blob/master/resources/images/fonts-conceal.png|Fonts with Conceal}} Fonts with Conceal More information about substitutions, including settings examples, can be found in the [[https://github.com/alygin/vscode-tlaplus/discussions/198|corresponding discussion]].