[Agda] agda2lagda (Halloween edition): Agda for the illiterate

[Andreas Abel]

Hello Agda community,

I found that I find writing literate Agda tedious, so I wrote a small tool

   https://andreasabel.github.io/agda2lagda/

that converts an ordinary Agda file into a LaTeX literate one, turning 
comments into text and program text into code blocks.  It also turns 
underlined text into headings.

Here is a small showcase:

   http://www.cse.chalmers.se/~abela/#cr-sk

   Strong normalization for simply-typed combinatory algebra using 
Girard’s reducibility candidates formalized in Agda

(Title, abstract and acknowledgements done in LaTeX, the main part comes 
from the Agda file.)

I imagine the following use case:  You started doing some Agda 
prototyping.  Then the project grows, and you consider a publication. 
You use agda2lagda to convert your code into literate code and continue 
from there.

Have fun!  --Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/