[Agda] lhs2tex and agda identifiers

[Nils Anders Danielsson]

On 2011-02-25 16:47, Dan Licata wrote:
> 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.

Interesting. Maybe Andres can explain what's going on.

-- 
/NAD