Literate Agda in Markdown format to LaTeX via Pandoc

Viewed 254

Agda supports Markdown for literate programming input, as described here: everything outside ``` and ```agda blocks is ignored by Agda, allowing you to load the same .lagda.md files into Agda and process them with Pandoc.

However, if Pandoc is used ultimately to target HTML output, then Agda can also be used do syntax highlighting and reference hyperlinking, as described in Jespec Cockx's blog post: agda --html produces valid Markdown from Markdown input, with all Agda code blocks replaced by HTML fragments that apply syntax highlighting.

Is there a way to do the same, but targeting LaTeX instead of HTML? So I'd like to do the following:

  1. Write Literate Agda in Markdown format in MySource.lagda.md file
  2. Process MySource.lagda.md with Agda to get Highlighted.md
  3. Process Highlighted.md with Pandoc, using the Beamer template, to produce Final.pdf.

I've tried using agda --latex for step 2, but its output file is byte-by-byte equal to the input file.

0 Answers
Related