[Agda] Unicode in Standard Library

[Andrés Sicard-Ramírez]

Hi Andreas,

On 12/02/2008, Andreas Abel <abel at cs.chalmers.se> wrote:
>
> 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?


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. A third option is to find
> the Unicode code point for the character (listed as U+XXXX) and enter
> the character using M-x ucs-insert.



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


In theory this solution should work, however I think it should be necessary
to add more information: the input method used,  the  sequence of
characters, and the information if this sequence of characters is defined or
not in the input method (because we can modify it).


All the best,



-- 
Andrés
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20080212/323a4fc1/attachment.html