[Agda] lhs2tex and agda identifiers

[Nils Anders Danielsson]

On 2011-02-25 00:46, Dan Licata wrote:
> 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?

Yes:

%format 1s = "\Varid{1}\mkern-3mu s"

-- 
/NAD