agda-blocks.hs

#!/usr/bin/env nix-shell
#!nix-shell -p "haskellPackages.ghcWithPackages (p: [ p.pandoc p.pandoc-types ])" -i runhaskell

{-# LANGUAGE OverloadedStrings #-}

import Text.Pandoc.JSON
import Text.Pandoc.Shared (tshow)
import Data.Text as T

main :: IO ()
main = toJSONFilter latexBlock

latexBlock :: Block -> Block
latexBlock x@(CodeBlock (_, l, _) b) =
  if l == ["agda"]
  then RawBlock "latex" (T.unlines ["\\begin{code}", b, "\\end{code}"])
  else x
latexBlock x = x

process.sh

pandoc Naturals.lagda.md -t latex -f gfm -F agda-blocks.hs

Requires specifying Agda as the language in the Markdown:

```agda
example
```