[Agda] Agda code in slides

[Nils Anders Danielsson]

On 2017-09-21 19:42, Sergei Meshveliani wrote:
> \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]

-- 
/NAD