Literate Programming

Agda supports a limited form of literate programming, i.e. code interspersed with prose, if the corresponding filename extension is used.

Literate TeX

Files ending in .lagda or .lagda.tex are interpreted as literate TeX files. All code has to appear in code blocks:

Ignored by Agda.

\begin{code}[ignored by Agda]
module Whatever where
-- Agda code goes here
\end{code}

Text outside of code blocks is ignored, as well as text right after \begin{code}, on the same line.

Agda finds code blocks by looking for the first instance of \begin{code} that is not preceded on the same line by % or \ (not counting \ followed by any code point), then (starting on the next line) the first instance of \end{code} that is preceded by nothing but spaces or tab characters (\t), and so on (always starting on the next line). Note that Agda does not try to figure out if, say, the LaTeX code changes the category code of %.

If you provide a suitable definition for the code environment, then literate Agda files can double as LaTeX document sources. Example definition:

\usepackage{fancyvrb}

\DefineVerbatimEnvironment
  {code}{Verbatim}
  {} % Add fancy options here if you like.

The LaTeX backend or the preprocessor lhs2TeX can also be used to produce LaTeX code from literate Agda files. See Known pitfalls and issues for how to make LaTeX accept Agda files using the UTF-8 character encoding.

Literate reStructuredText

Files ending in .lagda.rst are interpreted as literate reStructuredText files. Agda will parse code following a line ending in ::, as long as that line does not start with ..:

This line is ordinary text, which is ignored by Agda.

::

  module Whatever where
  -- Agda code goes here

Another non-code line.
::
.. This line is also ignored

reStructuredText source files can be turned into other formats such as HTML or LaTeX using Sphinx.

  • Code blocks inside an rST comment block will be type-checked by Agda, but not rendered.

  • Code blocks delimited by .. code-block:: agda or .. code-block:: lagda will be rendered, but not type-checked by Agda.

  • All lines inside a codeblock must be further indented than the first line of the code block.

  • Indentation must be consistent between code blocks. In other words, the file as a whole must be a valid Agda file if all the literate text is replaced by white space.

Literate Markdown and Typst

Files ending in .lagda.md are interpreted as literate Markdown files, while files ending in .lagda.typ are interpreted as literate Typst files. They use the same syntax for code blocks, and they are parsed the same way by Agda. Code blocks start with ``` or ```agda on its own line, and end with ```, also on its own line:

This line is ordinary text, which is ignored by Agda.

```
module Whatever where
-- Agda code goes here
```

Here is another code block:

```agda
data ℕ : Set where
 zero : ℕ
 suc  : ℕ → ℕ
```

For Typst, Agda does not yet support highlighting the code blocks.

Markdown source files can be turned into many other formats such as HTML or LaTeX using PanDoc.

  • Code blocks which should be type-checked by Agda but should not be visible when the Markdown is rendered may be enclosed in HTML comment delimiters (<!-- and -->).

  • Code blocks which should be ignored by Agda, but rendered in the final document may be indented by four spaces.

  • Note that inline code fragments are not supported due to the difficulty of interpreting their indentation level with respect to the rest of the file.

Only agda code blocks

Added in version 2.9.0.

By default, both unmarked code blocks (```) and explicitly marked code blocks (```agda) are treated as Agda code.

With the --literate-markdown-only-agda-blocks command-line option (off by default), only code blocks explicitly marked with ```agda are treated as Agda code. Unmarked code blocks are treated as verbatim text and are not type-checked. This allows including other code examples in the document without Agda attempting to parse them.

Example with --literate-markdown-only-agda-blocks:

This is prose.

Here is some Agda code:

```agda
data Bool : Set where
  true false : Bool
```

Here is a JavaScript example that is NOT type-checked:

```
function hello() { return "world"; }
```

Here is another verbatim block with a language tag:

```haskell
main = putStrLn "Hello, World!"
```

This option is not available as pragma since it affects parsing before any pragma options are processed. It must be set via command line (agda --literate-markdown-only-agda-blocks) or passed under flags: in the .agda-lib file.

Literate Org

Files ending in .lagda.org are interpreted as literate Org files. Code blocks are surrounded by two lines including only `#+begin_src agda2` and `#+end_src` (case-insensitive).

This line is ordinary text, which is ignored by Agda.

#+begin_src agda2
module Whatever where
-- Agda code goes here
#+end_src

Another non-code line.

  • Code blocks which should be ignored by Agda, but rendered in the final document may be placed in source blocks without the agda2 label.

Literate Forester

Files ending in .lagda.tree are interpreted as literate Forester files. Literate forester uses `\agda{...}` for code blocks.

  • Run agda --html --html-highlight=code example.lagda.tree to generate html/example.tree.

  • Add html/ to the trees list in forest.toml so Forester can find the generated trees.

  • Modify theme/tree.xsl of your forester project to include Agda.css in the linked stylesheets.

Running forester build produce file output/example/index.xml.

  • Run cp html/Agda.css output/, now you get Agda syntax highlighting.

\p{This line is ordinary text, which is ignored by Agda.}

\agda{
module Whatever where
-- Agda code goes here
}

\p{Here is another code block:}

\agda{
data ℕ : Set where
 zero : ℕ
 suc  : ℕ → ℕ
}

  • Self-link issue with Agda + Forester: When compiling .lagda.tree files, Agda generates links to local definitions using the module name (e.g., bool.html#232). However, Forester outputs pages as output/bool/index.html. This mismatch causes self-referential links to resolve to bool/bool.html#232 instead of #232 on the current page, resulting in 404s. This cannot be fixed in Agda’s HTML backend - it has no awareness of Forester’s output structure. A post-processing script is needed: for each generated page, copy output/i/index.html to output/i/i.html so the incorrect paths become valid redirects.

  • A similar problem occurs with references to Agda modules not compiled as part of your forest - whether standard library modules or local .agda files without corresponding trees. A script could rewrite these as root-relative paths (e.g., /Agda.Primitive.html#388), which works if you host at a domain root. But this isn’t general - on GitHub Pages, for example, your site lives at your-id.github.io/your-repo/, so the correct path would be /your-repo/Agda.Primitive.html#388 - requiring the script to know your deployment prefix. Either way, you also need to copy the generated HTML files from html/ to your output directory - Forester won’t include them automatically.