<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&#39;Connor <span dir="ltr">&lt;<a href="mailto:liamoc@cse.unsw.edu.au" target="_blank">liamoc@cse.unsw.edu.au</a>&gt;</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&#39; is printed as a lower index.</div><div>But I would like to have  list\_A  -- and identifier `list&#39; with `A&#39; </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>