What is the best way to type something like m≤n in Emacs's Agda mode?
If I type m \ < = n I get m≰, which is annoying.
My current workaround is to type m \ < = Space Backspace n but it is not very ergonomic.
Is there something I can do that doesn't require me to type an useless key and then immediately delete it with backspace?
Another option is to use Ctrl+g to exit the "character composition" mode.
So to inputm≤n you can type m \ < = (Ctrl+g) n
If you press C-u C-c = while your cursor is on the character, you will get information about it. The input line details the various ways in which you may input it.
Looks like \leqslant doesn't suffer from an additional n turning ≤ into ≰. However it is shorter to type space & then erase it.
