Generating HTML

To generate highlighted, hyperlinked web pages from source code, run the following command in a shell:

$ agda --html --html-dir={output directory} {root module}

You can change the way in which the code is highlighted by providing your own CSS file instead of the default, included one (use the --css option).


--html-dir directory
Changes the directory where the output is placed to directory. Default: html.
--css URL
The CSS file used by the HTML files (URL can be relative).