[Agda] Re: LaTeX-Backend: \renewcommand{\defaultcolumn}{...} shows no effect

[Stevan Andjelkovic]

Andreas Abel <abela at ...> writes:
>
> I found the space between the columns excessive.  After some research I 
> found
>
> [...]
>
>    \renewcommand{\defaultcolumn}{ <at> {~}l <at> {~}}

Yeah, I couldn't figure out how to change it -- thanks for looking into 
it. I found the excessive spacing after aligned stuff especially annoying.
Using your trick in conjunction with:

  \renewcommand{\AgdaIndent}[1]{\;\;}

results in output which is much nicer than what agda.sty currently
delivers by default. Does anyone know how to make it even nicer?
I opened a ticket in the bug tracker for discussing a change to the 
default:

  https://code.google.com/p/agda/issues/detail?id=955


Cheers,
SA.