[Agda] lhs2tex and agda identifiers

[Dan Licata]

On Feb25, Nils Anders Danielsson wrote:
> 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"
> 

Thanks! That helps.  Still a bit of weird behavior though: If I say 

data Type where 
    1s  : Type

then the 1s renders properly.

When I then say

  Element : Type -> Set
  Element 1s        = Unit

it renders as 

Element 1s s = Unit

If I put parens around the argument

Element (1s) = Unit

I get the right behavior though.

-Dan