[Agda] agda latex mode

[Thorsten Altenkirch]

I need to typeset some agda code for explanatory purposes in a lagda file, hence I don't want to type check it or include the definitions.

Now instead of hand translating agda code into Math I can let agda do the work and then copy the output from the late files that agda produces into my original file.
However, the problem is that I seem to need the code environment in the output but if I use it agda will try to translate it.

Hence my question is there a dummy version of code which I can use for this purpose?
E.g. I want to typeset something like
\begin{code}
\>[2]\AgdaFunction{proj₁}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{A}\AgdaSpace{}%
\AgdaBound{B}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitiveType{Set}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaOperator{\AgdaRecord{×}}\AgdaSpace{}%
\AgdaBound{B}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaBound{A}\<%
\end{code}

in my .lagda file. But obviously I can't do that.

If there is an even better way to achieve this I would also be interested. Maybe I better use lhs2tex afer all?

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 contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.