I am making Beamer slides for a talk about an Agda formalisation of mine.
In order to make the code fit onto the slide, I need to scale the font size. One would think that this might not be so hard, but the previous 20 tricks that I've tried all fail in the sense that, post compilation with
agda --latex, the relevant tricks simply disappear from the output file.
I tried setting the global document font size to the smallest possible option (and then using
\Huge for all remaining text), but
8pt on a Beamer project is still quite large and doesn't quite give me the room that I need.
Has anybody here ever been able to successfully change the code output size in a Literate Agda project?
P.S. There exists at least one absolutely unpalatable solution: hand modifying the output latex files.