[Agda] Re: lhs2TeX for agda

[Neil Sculthorpe]

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