Agda поддерживает Markdown для грамотного ввода программ, , как описано здесь : все, что находится за пределами блоков ``` и ```agda, игнорируется Agda, что позволяет загружать те же файлы .lagda.md в Agda и обрабатыватьих с Pandoc.
Однако, если Pandoc в конечном итоге используется для нацеливания на вывод HTML, Agda также может использоваться для подсветки синтаксиса и ссылки на гиперссылки, как описано в блоге Джеспека Кокса : agda --html создает действительную Markdown из ввода Markdown, при этом все блоки кода Agda заменяются фрагментами HTML, в которых применяется подсветка синтаксиса.
Есть ли способ сделать то же самое, но с ориентацией на LaTeX вместо HTML? Поэтому я хотел бы сделать следующее:
- Записать грамотную Агду в формате Markdown в
MySource.lagda.md файл - Обработать
MySource.lagda.md с Агдой, чтобы получить Highlighted.md - Обработка
Highlighted.md с помощью Pandoc с использованием шаблона Beamer для получения Final.pdf.
Я пытался использовать agda --latex для шага 2, но его выходной файл является побайтовым-байт равен входному файлу.