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

Safe HaskellNone
LanguageHaskell2010

Agda.Interaction.Highlighting.LaTeX

Description

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

Synopsis

Documentation

generateLaTeX :: Interface -> TCM () Source #

The only exported function.