[Agda] Re: lhs2TeX for agda

[Chantal Keller]

Hi Ondrej and Neil,

The LaTeX ucs package <http://www.unruh.de/DniQ/latex/unicode> is very 
useful to use unicode inside LaTeX source files.

Chantal.



Le 16/07/2010 18:13, Neil Sculthorpe a écrit :
>
> Hi Ondrej
>
> I've had that error too. I think it's objecting to unicode symbols.
>
> I'm not sure if lhs2tex is supposed to be able to handle unicode, but
> replacing them with ASCII should help. (And then writing a %format
> directive to turn them back into unicode).
>
> Neil
>
> On 16/07/10 16:38, Ondrej Rypacek wrote:
>> Hi Neil
>>
>> Thanks, that makes a difference, indeed. Now I'm getting (the last few
>> lines):
>>
>> ...
>>> \begin{document}
>>>
>>> We start with the module header:
>>> lhs2TeX: Enum.toEnum{Word8}: tag (8801) is outside of bounds (0,255)
>>
>> Cheers,
>> Ondrej
>>
>>
>>
>> On 16 July 2010 12:48, Neil Sculthorpe<nas at cs.nott.ac.uk> wrote:
>>> Hi Ondrej
>>>
>>> I got the same error after installing lhs2tex 1.15 (though I'm on
>>> Ubuntu).
>>>
>>> The problem seemed to be that the files in
>>> "/usr/local/share/lhs2tex-1.15/"
>>> (which includes Agda.fmt) were only readable by the user. Setting
>>> them to
>>> be readable by all solved it for me.
>>>
>>> Neil
>>>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>

-- 
Chantal KELLER