[Agda] xs\_A

[Liam O'Connor]

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 (mailto: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/51b683af/attachment-0001.html