Stream: VsCoq devs & users

Topic: inputting UTF8 symbols


view this post on Zulip Mukesh Tiwari (Sep 22 2021 at 11:30):

Hi @Théo Winterhalter, possibly a noob question but how do you input these pretty symbols (I tried \forall but it did nothing, so I am wondering how can I input these symbols via keyboard).

view this post on Zulip Théo Winterhalter (Sep 22 2021 at 11:31):

I personally use https://marketplace.visualstudio.com/items?itemName=yellpika.latex-input

view this post on Zulip Mukesh Tiwari (Sep 22 2021 at 11:32):

Awesome! Thank you very much.

view this post on Zulip Ralph Matthes (Jul 13 2022 at 15:18):

How would you relate that package to https://marketplace.visualstudio.com/items?itemName=oijaz.unicode-latex ?
I start typing backslash, then the first letters of the symbol description, and I get a menu to choose my symbol from - this is all in-place.

view this post on Zulip Meven Lennon-Bertrand (Aug 17 2022 at 09:03):

They look very similar to me. Your proposal seems to have a few more capabilities, like triggering a text-wide replacement. Also, their list of symbols to choose from are probably different (yours is based upon Julia’s list, while Théo’s one looks handcrafted to me, but can be modified by hand if needed)


Last updated: Jan 30 2023 at 17:03 UTC