[Agda] lhs2tex and agda identifiers

Dan Licata drl at cs.cmu.edu
Fri Feb 25 00:46:06 CET 2011


When I have an identifier that starts with a number, like 1s, lhs2tex
renders it with a space (e.g. "1 s"), presumably because it's not a
valid Haskell identifier.  

Is there any way to work around this, e.g. using a %format directive?

Thanks!
-Dan


More information about the Agda mailing list