[Agda] TeX capacity exceeded

Amr Sabry sabry at soic.indiana.edu
Thu Jan 9 22:42:50 CET 2014


I have been having serious problems when generating latex from
Agda. After generating a couple of pages of code, I get a "TeX capacity
exceeded". After looking at the tex configuration etc. I don't think the
error is from the tex side. I am including the lagda source and would
appreciate it if someone can test it and see if the latex output
compiles without errors. A copy of their memory configuration for tex
would be appreciated in that case. I am guessing the one number that
matters most is save_size. Thanks. --Amr

P.S. If I remove either of the last two definitions (apfInv or apfComp),
I can produce a pdf without errors. So I know each definition is correct
by itself. When both definitions are included I get the error. Thanks
again.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: circle.lagda
Type: application/octet-stream
Size: 5778 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20140109/0113a12e/circle.obj


More information about the Agda mailing list