[Agda] Unicode in Standard Library

[Andreas Abel]

Dear AIs, [think of AIM!]

the new standard library seems quite nice, with ambitious use of unicode 
characters.  My tiny problem is:  how can I use it when I have no key 
for ℕ on my keyboard?

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

Cheers,
Andreas

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

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/