[Agda] xs\_A

Serge D. Mechveliani mechvel at botik.ru
Tue Feb 5 11:42:43 CET 2013


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


More information about the Agda mailing list