Safe Haskell | None |
---|---|
Language | Haskell2010 |
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.