Stream: VsCoq devs & users

Topic: Shift-Space (latex to unicode)?

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: Jan 30 2023 at 17:03 UTC