agdaagda-mode

Agda mode not converting unicode commands to symbols

I recently installed (or at least think I have) agda and agda-mode. The problem is that when I type a symbol like "\to" or "\bV" on Emacs, they stay that way and don't convert to the desired symbol. But when I copy paste it from outside the application, they show perfectly fine. Im not sure what Im doing wrong since it seems that I have agda and agda-mode installed:

enter image description here

enter image description here

I also tried doing

Alt+X
set-input-method
Agda

But still when I write something like "\forall" it stays that way and doesn't convert to a symbol.

Im using agda 2.6.4.1 and Emacs 29.2 on Windows 10.

Solution

  • OK I think I found the issue. I was copy-pasting the backlash \ instead of manually inserting it because "Ctrl+Alt+' " or Alt+92 conflicts with Emacs shortcuts. And turns out that pasting the backlash instead of manually typing it doesn't trigger emacs-mode. You have to manually insert the backlash using the keyboard instead of pasting it -.-. So that was it.