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

[Alan Jeffrey]

\defaultcolumn is the command to set the default column, so by using 
\renewcommand{\defaultcolumn}{...} you're redefining the command that 
sets the default column, not redefining the default column itself. You 
should be able to use \defaultcolumn{...} in your own LaTeX file, you 
shouldn't have to edit agda.sty.

A.

On 11/12/2013 07:48 AM, Andreas Abel wrote:
> 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
> found
>
>    \defaultcolumn{l}
>
> in agda.sty.  I tried the following
>
>    \usepackage{latex/agda}
>    \renewcommand{\defaultcolumn}{@{~}l@{~}}
>
> but to no avail.  By chance I found out that if I modify the command in
> agda.sty, to
>
>    \defaultcolumn{@{~}l@{~}}
>
> everything works as excepted.
>
> Why did \renewcommand{...} show no effect?  (I always thought that LaTeX
> has dynamic binding...)
>
> Cheers,
> Andreas
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda