[Agda] Re: lhs2TeX for agda

Ondrej Rypacek ondrej.rypacek at gmail.com
Fri Jul 16 17:38:06 CEST 2010


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
>


More information about the Agda mailing list