[Agda] Agda code in slides

[Guillaume Allais]

Hi Sergei,

Have you had a look at the wiki on this topic? It's full on neat
tricks e.g. the use of the catchfilebetweentags package:

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.LiterateAgda

Cheers,
--
gallais

On 21/09/17 19:42, Sergei Meshveliani wrote:
> People,
>
> I need to prepare a slide presentation in LaTex which has many fragments
> of Agda code.
> I write (as an example) 
>
> ----------------------------------------------
> \documentclass[pdf]{beamer}
> \mode<presentation>{}
>
> % This handles the translation of unicode to latex:
> \usepackage{ucs}
> \usepackage[utf8x]{inputenc}
> \usepackage{autofe}
> ...
>
> \begin{document}
> \title{Foo}
> \author{Foo}
> \maketitle
>
> \begin{frame}{Foo}
>
> \begin{verbatim}
>   record Foo : Set where
>          constructor foo'
>          field
>            a   :  Rel C _
>            op₂ :  C → C
>            a≉0 :  a ≉ 0#
>
>   _='_ :  Rel C _
>   x =' y =  (f x * f y) ≈ y
> \end{verbatim}
> \end{frame}
> \end{document}
> ----------------------------------------------
>
> And  pdflatex reports errors.
> Removing  {verbatim}  makes it compiled. But this breaks the code
> script, indentations, frame nicety, etc.
>
> What is, please, a way out?
>
> Thanks, 
>
> ------
> Sergei
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170922/293f81cf/attachment-0001.sig>