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

Safe Haskell | None

Agda.Interaction.Highlighting.LaTeX

Description

Function for generating highlighted and aligned LaTeX from literate Agda source.

Synopsis

- generateLaTeX :: ModuleName -> HighlightingInfo -> TCM ()

# Documentation

generateLaTeX :: ModuleName -> HighlightingInfo -> TCM ()

The only exported function. It's (only) called in `Main.hs`.