[Agda] xs\_A

[Jean-Philippe Bernardy]

Enjoy.

http://en.wikipedia.org/wiki/Unicode_subscripts_and_superscripts

-- JP


On Tue, Feb 5, 2013 at 11:45 AM, Liam O'Connor <liamoc at cse.unsw.edu.au>wrote:

>  the \_1 is just a unicode subscript character. No other subscripts are
> supported, as far as i know.
>
> Cheers,
> Liam
>
> On Tuesday, 5 February 2013 at 9:42 PM, Serge D. Mechveliani wrote:
>
> People,
> Is it possible in Agda and agda-mode for emacs to write in
> identifiers lower (upper) index letters other than didits?
>
> For example, I try to write list\_1 instead of list-A, and this
> identifier does work, and `1' is printed as a lower index.
> But I would like to have list\_A -- and identifier `list' with `A'
> printed as the position of a lower index.
> And the agda mode does not understand my attempts with
> list\_a, list\_A, list\_{A}.
>
> Thanks,
>
> ------
> Sergei
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130205/5e07d0d7/attachment.html