Creating Latex Output from Agda Files

• It might be useful to create a directory tex in which Latex output is stored: Execute in a shell
  mkdir tex
• 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 "view".
• Choose menu File -> PrintToFile.
• Choose a suitable file name
  • (it's better to replace <filename>.agda.tex by <filename>.tex),
  and save it in the directory tex.
• 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 font size.
• Now execute in a shell latex on this file:
  latex <filename>header
• You can view it by executing
  xdvi <filename>header
• You can print it using
  dvips <filename>header