Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.Interaction.Highlighting.HTML

Description

Function for generating highlighted, hyperlinked HTML from Agda sources.

Synopsis

- generateHTML :: ModuleName -> TCM ()

# 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.