[Agda] agda --latex inline code

[Stevan Andjelkovic]

On Fri, May 09, 2014 at 01:57:56PM +0100, Altenkirch Thorsten wrote:
> However, is there a way to write inline Agda code as |..| in lhs? 

The backend only typesets code inside code blocks, inline code you
have to typeset manually, e.g.:

  Below we postulate a set called \AgdaDatatype{apa}.

  \begin{code}
  postulate apa : Set
  \end{code}

You can find all the commands used by the backend (and which you can use
manually) in the latex/agda.sty file. If you are doing a lot of manual
typesetting, then you might want to introduce shorter command names,
e.g.:

  \newcommand{\D}{\AgdaDatatype}
  \newcommand{\F}{\AgdaFunction}

etc, I chose long names to avoid name clashes.

> Also sometimes (especially when explaining Agda syntax), I don't
> actually want to type check my code but just produce latex. Is this
> possible?

Typechecking is essential to the typesetting (otherwise we don't
know what colours etc to use). 

However, since lhs2tex and the latex backend are interchangeable (or
should be at least), I suppose you could have a "fast" and a "slow"
make target, e.g. a Makefile with:

  COMPILER=latexmk -pdf -use-make -e '$$pdflatex=q/xelatex %O %S/'

  fast:
        lhs2tex --agda <file>.lagda > latex/<file>.tex
        cd latex && \
        $(COMPILER) <file>.tex && \
        mv <file>.pdf ..

  slow:
        agda --latex <file>.lagda
        cd latex && \
        $(COMPILER) <file>.tex && \
        mv <file>.pdf ..
        
Then you can compile using "make fast" to avoid typechecking (at the cost
of not having colours etc).

I don't use this setup myself, so I don't know how well it works in
practice... 


Cheers,
SA.