<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>
<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">Agda@lists.chalmers.se</a></div><div><a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a></div></div></div></span>
</blockquote>
<div>
<br>
</div>