[Agda] beamer + latex mode + font sizes

[Jacques Carette]

On 2016-04-05 15:10 , Andrés Sicard-Ramírez wrote:
> On 4 April 2016 at 11:30, Jacques Carette <carette at mcmaster.ca> wrote:
>> I am trying to control the font size of agda code block in .lagda files
>> in a beamer presentation, and not succeeding.
>>
>> I have tried:
>> 1. using
>> {\tiny{
>> \begin{code}
>> ...
>> \end{code}}}
> The following code works for me (tested with Agda 2.4.2.5 and pdflatex):
>
> \tiny
> \begin{code}
> ...
> \end{code}
> \normalsize
>
>

I eventually discovered that buried in my preamble, I had
\renewcommand{\AgdaCodeStyle}{\small}

which is what prevented the other methods from working properly. Now 
that I have removed that, the standard ways started working!

Jacques