3

How could I write literate (and exportable to latex) Agda code in org-mode?

  • Org-babel would be a great option, but there is no ob-agda2 (I think?). I have tried defining an org-babel-execute function for agda following the template ob-template.el, but my knowledge of Elisp is not enough to fill all the required functions.
  • Literate Agda works well with Latex files, but it needs the extension of the file to be .lagda and only detects Agda code between \begin{code} ... \end{code}, instead of the org-mode syntax of #+begin_src agda2.

A possible solution right now would be to add some Latex export options to make \begin{code} export correctly to Latex 

#+latex_header: \usepackage{verbatim} #+latex_header: \newenvironment{code}{\verbatim}{\endverbatim}

and to keep changing betweeen major modes (org and agda) to edit the same file, with an .org.lagda extension. Is there any better way to do this?

Improve this question
1
  • The solution on the "Using beamer..." section of this page works. The pdf compilation gets a bit complex, but the final result is perfect. I still would like to ask if there is a simpler way using org-babel or keeping only one file. Commented Jun 4, 2017 at 22:43

1 Answer 1

Reset to default
0

Since I found my way to this question it seems others might. This is now available out of the box. See: https://agda.readthedocs.io/en/latest/tools/literate-programming.html#literate-org

Improve this answer

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.