Can't get conversion of ASCII symbols to Latex-like symbols

[andrewlubrino]

I'm pretty sure I have everything installed correctly, but I can't get the nice-looking implication, conjunction, disjunction, etc. symbols to appear in my VSCode window. Any ideas on how to troubleshoot? I'm running this on a Chromebook with developer mode enabled, so this is basically running on some flavor of Linux. A screenshot of my VSCode is below:

[infogulch]

You mean ligatures? You need a font that supports ligatures (e.g. Iosevka) and to set "editor.fontLigatures": true, in settings.json.

[digama0]

Sorry for the bad news, but MM0 does not support Unicode (deliberately, because specifying unicode is a nightmare). The MM1 proof assistant allows it but only in comments. (It might one day be extended to everywhere except notations and public theorems, since it has to talk to MM0 which is unicode-free.) The font I use in the tutorial video and in my day-to-day work is Fira Code, and you have to enable ligatures to use it in VSCode.

[andrewlubrino]

Okay, so I downloaded Fira Code and installed in one of the fonts directories. My settings.json file is below:

{
    "workbench.colorTheme": "Default Dark+",
    "metamath-zero.executablePath": "/home/andrewlubrino/mm0/mm0-rs/target/release/mm0-rs",
    "editor.fontLigatures": true,
    "editor.fontFamily": "'Fira Code','Droid Sans Mono', 'monospace', monospace,"
}

I'm still having no luck. Any other tips? Thanks for the help.

[andrewlubrino]

I'm not sure what Unicode is, but I just want to basically get the nice-looking implication symbol from Mario's youtube video introducing MM0.

[andrewlubrino]

I got it! So exciting. Thanks again.