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

Safe HaskellNone
LanguageHaskell98

Agda.Interaction.Highlighting.LaTeX

Description

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

Synopsis

Documentation

generateLaTeX :: TopLevelModuleName -> HighlightingInfo -> TCM () Source

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