[Agda] TeX capacity exceeded

[Andres Loeh]

Hi.

I can reproduce this (with Agda 2.3.2). Quickly scanning the generated
LaTeX output, I find (within a single code block):

\>[2]\AgdaIndent{4}{}\<[4]%

[...]

\>[4]\AgdaIndent{2}{}\<[2]%

These two lines create a cycle between the column labelled "2" and
"4", and polytable.sty's sorting algorithm will loop (it unfortunately
doesn't check for cycles). If Andreas says that this doesn't occur
with the latest Agda, then perhaps the LaTeX code generator has been
improved/fixed in the meantime.

Cheers,
  Andres