Haskell (Jan 05 2021 at 12:40): Haskell (Jan 05 2021 at 12:40):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.
Théo Winterhalter (Jan 05 2021 at 12:49):I personally use latex-input to input commands. You just have to type \to or \pi and the interface will suggest the corresponding unicode symbol, without having to switch modes or use a specific command.
Haskell (Jan 05 2021 at 14:42):Thank you, I switched to that as well!
Last updated: Jun 04 2023 at 23:30 UTC