[Agda] Writing a paper in Literate Agda

[Mateusz Kowalczyk]

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.