[Agda] Unicode in Standard Library

[Shin-Cheng Mu]

On 12 Feb 2008, Andr?s Sicard-Ram?rez wrote:
> I had the same tiny problem some weeks ago and this was the Nils's  
> answer:
>> Either you can modify the TeX input method so that it handles these
>> characters (see the Agda README file), or you can use C-u C-x = with
>> another input method active (for instance ucs or rfc1345) to see how
>> to enter the characters using that method. ...

It is probably a good idea to have a "standard prelude"
for .emacs with a selection of default key bindings
which mainly covers the symbols used in the standard
library. It could be a bit inconvenient if everyone
define their own key bindings and people are able to
write Agda programs only on their own computers.

sincerely,
Shin