Hi Andreas,<br><br><div><span class="gmail_quote">On 12/02/2008, <b class="gmail_sendername">Andreas Abel</b> <<a href="mailto:abel@cs.chalmers.se">abel@cs.chalmers.se</a>> wrote:</span><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
Dear AIs, [think of AIM!]<br><br>the new standard library seems quite nice, with ambitious use of unicode<br>characters. My tiny problem is: how can I use it when I have no key<br>for ℕ on my keyboard?</blockquote><div>
<br>I had the same tiny problem some weeks ago and this was the Nils's answer: </div><br><span class="q"><span class="gmail_quote"></span><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<br>Either you can modify the TeX input method so that it handles these<br>characters (see the Agda README file), or you can use C-u C-x = with<br>another input method active (for instance ucs or rfc1345) to see how<br>to enter the characters using that method. A third option is to find
<br>the Unicode code point for the character (listed as U+XXXX) and enter<br>the character using M-x ucs-insert.</blockquote></span><br><br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
Possible fix: at the definition of a new unicode identifier, add a<br>comment how to type it.</blockquote><div><br>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).<br>
<br> <br>All the best,<br><br></div></div><br><br>-- <br>Andrés