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¶

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 ().
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.

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.