[Agda] include agda in latex

[Dominique Devriese]

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...

Regards,
Dominique

2014/1/13 Altenkirch Thorsten <psztxa at exmail.nottingham.ac.uk>:
> AFAIK, the standard way to combine agda with latex is to write an lagda file
> and then use either lhs2tex or the new latex flag to create a latex file
> which contains nicely typeset agda code.
>
> However, I find myself frequently in the situation that I want to include
> some agda code in a larger latex document, e.g. some slides but I am
> hesitant to turn my whole latex file into a lagda file because then I always
> have to apply the preprocessor each time I want to latex my file which
> disables certain useful support, e.g. using C-c C-r in emacs. Also the agda
> code is usually incomplete and I am not going to  really want to process the
> whole file with agda.
>
> Obviously one thing I can do is to produce a pdf file from printing my agda
> code and include it in my talk. However, this has some disadvantage – the
> fonts may not match and I have to do this again by hand each time I change
> my agda file.
>
> So is there a way to do this now (include agda latex in my file w.o. turning
> everything into an agda project)? Or, if not what would one need to do to
> facilitate this.
>
> Thorsten
>
> This message and any attachment are intended solely for the addressee and
> may contain confidential information. If you have received this message in
> error, please send it back to me, and immediately delete it.   Please do not
> use, copy or disclose the information contained in this message or in any
> attachment.  Any views or opinions expressed by the author of this email do
> not necessarily reflect the views of the University of Nottingham.
>
> This message has been checked for viruses but the contents of an attachment
> may still contain software viruses which could damage your computer system,
> you are advised to perform your own checks. Email communications with the
> University of Nottingham may be monitored as permitted by UK legislation.
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>