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

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.