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

[Andreas Abel]

Ah, yes, of course.  That was idiosyncratic.  Thanks!

Somehow I am used to overwrite commands in LaTeX to configure stuff, like in

   \def\arraystretch{1.5}

so this did not occur to me.

Cheers,
Andreas

On 12.11.2013 15:11, Alan Jeffrey wrote:
> \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


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/