<div dir="ltr">Enjoy.<div><br></div><div><a href="http://en.wikipedia.org/wiki/Unicode_subscripts_and_superscripts">http://en.wikipedia.org/wiki/Unicode_subscripts_and_superscripts</a><br></div><div><br></div><div style>-- JP</div>
</div><div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, Feb 5, 2013 at 11:45 AM, Liam O'Connor <span dir="ltr"><<a href="mailto:liamoc@cse.unsw.edu.au" target="_blank">liamoc@cse.unsw.edu.au</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div>
the \_1 is just a unicode subscript character. No other subscripts are supported, as far as i know.
</div>
<div><div><br></div><div>Cheers,</div><div>Liam</div><div><br></div></div><div class="HOEnZb"><div class="h5">
<p style="color:#a0a0a8">On Tuesday, 5 February 2013 at 9:42 PM, Serge D. Mechveliani wrote:</p>
<blockquote type="cite" style="border-left-style:solid;border-width:1px;margin-left:0px;padding-left:10px">
<span><div><div><div>People,</div><div>Is it possible in Agda and agda-mode for emacs to write in </div><div>identifiers lower (upper) index letters other than didits?</div><div><br></div><div>For example, I try to write list\_1 instead of list-A, and this </div>
<div>identifier does work, and `1' is printed as a lower index.</div><div>But I would like to have list\_A -- and identifier `list' with `A' </div><div>printed as the position of a lower index. </div><div>And the agda mode does not understand my attempts with </div>
<div>list\_a, list\_A, list\_{A}.</div><div><br></div><div>Thanks,</div><div><br></div><div>------</div><div>Sergei</div><div>_______________________________________________</div><div>Agda mailing list</div><div><a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a></div>
<div><a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a></div></div></div></span>
</blockquote>
<div>
<br>
</div>
</div></div><br>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>