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

Andreas Abel abela at chalmers.se
Tue Nov 12 14:48:21 CET 2013

Hi to the users of Agda's LaTeX-Backend,

this is a very nice tool, I am using it for the first time.

I found the space between the columns excessive.  After some research I 


in agda.sty.  I tried the following


but to no avail.  By chance I found out that if I modify the command in 
agda.sty, to


everything works as excepted.

Why did \renewcommand{...} show no effect?  (I always thought that LaTeX 
has dynamic binding...)


More information about the Agda mailing list