[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