TLDR; Press C-\ and try again

Adga documentation claims that typing <kbd>\to</kbd> will insert a spiffy unicode arrow ("→"), but you only see \to staring back at you. And if you find an Agda screencast, you can tell that it's supposed to be an easy, automatic process.

Basically, if you press <kbd>\</kbd> and you don't see , you may be running into the same problem that I had: the "Agda input method" is probably disabled. Try toggling the input method by pressing C-\—you should see an upper-case Pi symbol appear at the left of the mode-line .

In my specific case, I figured out that Evil was the culprit. I'm not exactly sure how it interferes, but disabling Evil indeed resulted in Agda's input method being enabled by default for Agda buffers.

For posterity's sake, the versions were: Agda 2.3.2.2; Emacs 23.4; and Evil 1.0.8.