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 LaTeX 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.