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. 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 tex code from literate Agda files. See Unicode and pdfLaTeX 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

Files ending in .lagda.md are interpreted as literate Markdown files. 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  :```

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.