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?

  • 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. – Mario Román Jun 4 '17 at 22:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.