[Agda] Agda code in slides

[Sergei Meshveliani]

On Fri, 2017-09-22 at 14:55 +0200, Nils Anders Danielsson wrote:
> 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]


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

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

------ 
Sergei