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

Andreas Abel andreas.abel at ifi.lmu.de
Tue Nov 12 17:54:09 CET 2013

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

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


so this did not occur to me.


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

More information about the Agda mailing list