[Agda] Agda code in slides

[Sergei Meshveliani]

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

[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

Post by Sergei Meshveliani
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>{}
\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
https://lists.chalmers.se/mailman/listinfo/agda

[Nils Anders Danielsson]

Post by Sergei Meshveliani
\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}

I seem to recall that if you want to use the verbatim environment inside
a frame, then the frame should be marked as fragile:

\begin{frame}[fragile]

[Sergei Meshveliani]

Post by Nils Anders Danielsson

Post by Sergei Meshveliani
\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}

I seem to recall that if you want to use the verbatim environment inside
\begin{frame}[fragile]

Thank you very much! This occurs the simplest way out.

Also thanks to people who responded, I store their advices as a reserve.

------
Sergei