Agda.Interaction.Highlighting.HTML

Function for generating highlighted, hyperlinked HTML from Agda sources.

Documentation

generateHTML :: ModuleName -> TCM ()

Generates HTML files from all the sources which the given module depends on (including the module itself).

This function should only be called after type checking has completed successfully.