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

Stevan Andjelkovic stevan.andjelkovic at strath.ac.uk
Tue Nov 12 18:04:43 CET 2013

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:


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 



More information about the Agda mailing list