[Agda] Spanish keyboard + Agda input-mode

[Michael Shulman]

I have a student who is trying to install Agda on his Mac (using
Aquamacs).  However, his computer (like himself) is from Spain, and
lacks a backslash key.  There is a key combination which lets him type
a backslash character, but it doesn't drop him into the agda
input-mode for typing unicode characters; it just prints a backslash.
I don't understand enough about how *macs input-modes work to fix it;
there doesn't seem to be an elisp function that I can bind to another
key.  Any suggestions?