[Agda] Unicode in Standard Library

[IKEGAMI Daisuke]

Dear Abel and all friends of Agda2,

> the new standard library seems quite nice, with ambitious use of unicode 
> characters.  
We are also happy that it is enable to use the Unicode characters. Great.

> My tiny problem is:  how can I use it when I have no key 
> for $,1uU(B on my keyboard?

I've never used the German keyboard, which the Emacs calls it as 'pc102-de'.
However, I know that the keyboard unfortunately does not have the key '?'.

This is a cheat memo for the 'pc102-de':

[pc102-de]
character | type key 
------------------------------------------------
  ?       | [-=] + Shift (i.e. the 'ss' + Shift)
  ;       | [,]  + Shift
  :       | [.]  | Shift
  -       | [/?]
------------------------------------------------

> P.S.: I see it coming: in a not to distant futures, I will have to 
> maintain code with Chinese identifiers.  Ni hao!

To edit Chinese characters, you know, we have to change the setting of Emacs:
  (set-language-environment "Chinese-GB") ; for the Simplified Chinese Characters
  (setq default-input-method "chinese-py-punct")
  (setq quail-keyboard-layout-type "pc102-de") ; if you use the German keyboard

To display the Chinese character, you have to use Emacs on X, 
otherwise set encoding of your terminal correctly.

> Possible fix: at the definition of a new unicode identifier, add a 
> comment how to type it.

I agree that you points a general way about the Unicode issue.

I wish this helps you. 'Jia You, Jia You!'
;; A Chinese tip: "Jia you" means 'Cheers', which is also means 'Add oil'

Ike