[Agda] beamer + latex mode + font sizes

[Andrés Sicard-Ramírez]

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


-- 
Andrés