Agda.Interaction.Highlighting.HTML

Function for generating highlighted, hyperlinked HTML from Agda sources.

Documentation

generateHTML :: TCM ()

Generates HTML files from all the sources which have been visited during the type checking phase.

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