# Literate agda programming in org-mode

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}

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?