[Agda] literate Agda with unicode in latex

[Martin Escardo]

More precisely, this is about literate Agda with unicode in latex in 
ubuntu with texlive.

The instructions at

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

didn't quite work for me. This is what works for me (presented as a 
complete latex file with an Agda hole):


\documentclass{article}

% The following packages are needed because unicode
% is translated (using the next set of packages) to
% latex commands. You may need more packages if you
% use more unicode characters:

\usepackage{amssymb}
\usepackage{bbm}
\usepackage[greek,english]{babel}

% These are the lines the Agda wiki tells you to add, to
% handle the translation of unicode to latex:

\usepackage{ucs}
\usepackage[utf8x]{inputenc} % (Not just "utf8".)
\usepackage{autofe}

% Some characters that are not automatically defined
% (you figure out by the latex compilation errors you get),
% and you need to define:

\DeclareUnicodeCharacter{8988}{\ensuremath{\ulcorner}}
\DeclareUnicodeCharacter{8989}{\ensuremath{\urcorner}}
\DeclareUnicodeCharacter{8803}{\ensuremath{\overline{\equiv}}}

% Add more as you need them.

% Using "\newenvironment" to redefine verbatim to
% be called "code" doesn't work. Hence instead:

\usepackage{fancyvrb}

\DefineVerbatimEnvironment
   {code}{Verbatim}
   {} % Add fancy options here if you like.

\begin{document}

\begin{code}
   ... your Agda code goes here ...
\end{code}

\end{document}

I hope this helps. Of course, this is not restricted to Agda.

Regards.