<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>