[Agda] Writing a paper in Literate Agda

Mateusz Kowalczyk fuuzetsu at fuuzetsu.co.uk
Fri Nov 29 02:37:30 CET 2013

On 29/11/13 00:19, Abhishek Anand wrote:
> Sorry for asking a beginner question.(Can't seem to find it on google).
> How does one generate a .lagda file from a .agda file
> When I compile in windows, I get a .exe file
> I also see some .agdai files

You don't generate .lagda files, you write your code in them. So for
example, instead of writing in MyModule.agda, you would write in
MyModule.lagda and then compile that. The difference is that you can use
the literate syntax when using the .lagda file extension and the
compiler should know what to do when it sees .lagda.

Mateusz K.

More information about the Agda mailing list