markdown - 通过 Pandoc 将 Markdown 格式的 Agda 读写到 LaTeX

Question

Agda 支持 Markdown 用于文学编程输入，如下所述：Agda 忽略外部的所有内容```和```agda块，允许您将相同的.lagda.md文件加载到 Agda 并使用 Pandoc 处理它们。

然而，如果 Pandoc 最终用于 HTML 输出，那么 Agda 也可以用于语法高亮和引用超链接，如Jespec Cockx 的博客文章所述：agda --html从 Markdown 输入生成有效的 Markdown，所有 Agda 代码块都替换为 HTML 片段应用语法高亮。

有没有办法做同样的事情，但针对 LaTeX 而不是 HTML？所以我想做以下事情：

1. MySource.lagda.md在文件中以 Markdown 格式编写 Literate Agda
2. 使用 Agda处理MySource.lagda.md以获得Highlighted.md
3. 使用 Beamer 模板与 Pandoc 进行处理Highlighted.md，以生成Final.pdf.

我已经尝试使用agda --latex第 2 步，但它的输出文件是逐字节等于输入文件的。

标签： markdownsyntax-highlightingpandocagdaliterate-programming