[Agda] Re: include agda in latex

[Stevan Andjelkovic]

Dominique Devriese <dominique.devriese at ...> writes:
> 
> Thorsten,
> 
> I sometimes use emacs's htmlize-buffer function on type-checked agda
> code to turn the highlighted code into a html file. This is useful for
> example to include highlighted agda code in an OpenOffice presentation
> (when I don't want to be bothered with latex beamer oddities).
> Perhaps, for your situation, there is a way to turn the html file from
> htmlize-buffer into latex code that can be included in a non-lhs2TeX
> latex file?
> 
> Anyway, if I understand correctly, the latex backend will make Agda
> output latex code directly, which seems like a cleaner approach, but I
> haven't used it and don't know how stable it is...

Hi,

Here is how I'd do it using the LaTeX-backend:

  * presentation.tex:

    \documentclass{beamer}
     
    \usepackage{latex/agda}
    \usepackage{catchfilebetweentags}
     
    \begin{document}
    \begin{frame}\frametitle{Some Agda code}
     
      \begin{itemize}
        \item The natural numbers
      \end{itemize}
     
      \ExecuteMetaData[latex/Code.tex]{nat}
     
      \begin{itemize}
        \item Addition (\AgdaFunction{\_+\_})
      \end{itemize}
     
      \ExecuteMetaData[latex/Code.tex]{plus}
     
    \end{frame}
    \end{document}

  * Code.lagda:

    %<*nat>
    \begin{code}
    data ℕ : Set where
      zero  : ℕ
      suc   : (n : ℕ) → ℕ
    \end{code}
    %</nat>
     
    %<*plus>
    \begin{code}
    _+_ : ℕ → ℕ → ℕ
    zero   + n = n
    suc m  + n = suc (m + n)
    \end{code}
    %</plus>
  
  * Makefile:

    SOURCE=presentation
    CODE=Code
     
    all:
        agda --latex $(CODE).lagda
     	latexmk -pdf -use-make $(SOURCE).tex

    tex:
     	latexmk -pdf -use-make $(SOURCE).tex
     
    clean:
     	rm -f $(CODE).agdai
     	rm -fr latex/


The \ExecuteMetaData command is part of the neat
catchfilebetweentags package, which you can read more about here:

 
http://mirrors.ctan.org/macros/latex/contrib/catchfilebetweentags/catchfilebetweentags.pdf
  
Hopefully the rest is clear.


Cheers,
SA.