Creating Latex Output from Agda Files
If one has installed Alfa and latex, one can create nice Latex output from
Agda as follows:
- It might be useful to create a directory tex in which Latex output is stored: Execute in a shell
- Now start alfa and open your Agda file you have created.
- You might change the layout of your file by using options provided in the menu item
- Choose menu File -> PrintToFile.
- Choose a suitable file name
and save it in the directory
- (it's better to replace <filename>.agda.tex by
- Save the file headerfile.tex as <filename>header.tex
in the directory tex.
- Open the file <filename>header.tex using an editor.
- Substitute "filename" in line 4 by the name of the file created by alfa.
- You might replace "12pt" in the first line by "10pt" or "11pt" to get a different
- Now execute in a shell latex on this file:
- You can view it by executing
- You can print it using
Last modified: Thu Jan 22 00:57:43 GMT 2004