Agda-mode will translate from symbol names to unicode for you. For example, \\to gets translated to → and \\== goes to ≡. It is very easy to work with after a s

Agda-mode will translate from symbol names to unicode for you. For example, \\to gets translated to → and \\== goes to ≡. It is very easy to work with after a short learning curve. There is more explanation available on the Agda Wiki. [0] [0] http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.UnicodeInput http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.Unicod...