[Agda] lhs2tex and agda identifiers

[Andres Loeh]

Hi.

With

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

there's the following problem:

>> 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.

The token "1s" isn't actually accepted as a single token by lhs2TeX,
even in Agda mode. The format directive

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

is actually interpreted as a parameterized format directive for 1,
where the parameter is called s. Now, "Element 1s" is parsed as
"Element" applied to "1" and "s". lhs2TeX will happily apply
formatting directives even if not all parameters are specified, so "1"
is typeset as "1s", followed by an extra "s". Parentheses can help
here. However, most likely you don't want to format all occurrences of
"1" as "1s", so even the parentheses aren't a good workaround.

It's better to actually choose a name that is a proper lhs2TeX token
for the identifier, and just use "1s" as the formatting on the TeX
side.

And yes, this is a bug. I've added it to my TODO list.

Cheers,
  Andres