Hi, I'm used to CoqIDE's latex to unicode translation on pressing Shift-Space. Is there a way to do this with VSCoq?
I do see an extension https://marketplace.visualstudio.com/items?itemName=oijaz.unicode-latex which I'll do bindings for if there isn't a "native" way to do this. Thanks.
I personally use
latex-input to input commands. You just have to type
\pi and the interface will suggest the corresponding unicode symbol, without having to switch modes or use a specific command.
Thank you, I switched to that as well!
Last updated: Jun 04 2023 at 23:30 UTC