[Agda] include agda in latex

[Abhishek Anand]

On Mon, Jan 13, 2014 at 9:09 AM, Altenkirch Thorsten <
psztxa at exmail.nottingham.ac.uk> wrote:

> 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
>
You dont need to do that. You can just use \input{agda_file.tex} in the
larger latex document to include the agda code
in agda_file.lagda (after running agda --latex)

In agda_file.lagda, do not put the latex preamble , e.g \begin{document} ,
\usepackage e.t.c
I just add the following to the preamble my main latex document:

\usepackage{agda}

\DeclareUnicodeCharacter{931}{$\sum$}

 \usepackage{autofe}


Then, in the lagda file, I just have \begin{code} .. \end{code} and
possibly some comments in between.
I just confirmed that C-c C-r keyboard shortcut to refine works in my lagda
file


>  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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140113/38d6399c/attachment-0001.html