| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Interaction.Highlighting.LaTeX
Description
Function for generating highlighted and aligned LaTeX from literate Agda source.
Synopsis
- generateLaTeX :: Interface -> TCM ()
Documentation
generateLaTeX :: Interface -> TCM () Source #
Generates a LaTeX file for the given interface.
The underlying source file is assumed to match the interface, but this is not checked. TODO: Fix this problem, perhaps by storing the source code in the interface.