Documentation

List of valid extensions for literate Agda files, and their corresponding preprocessors.

If you add new extensions, remember to update test/Utils.hs so that test cases ending in the new extensions are found.

The Bool parameter controls whether only ```agda blocks are treated as Agda code in Markdown/Typst files. When True, only blocks marked ```agda are considered code. When False, both ``` and ```agda blocks are code (default).

List of valid literate file extensions.

Preprocessor for literate TeX.

Preprocessor for reStructuredText.

Preprocessor for Markdown.

The Bool parameter controls whether only ```agda blocks are treated as Agda code. When True, only blocks explicitly marked ```agda are considered code. When False, both unmarked ``` and ```agda blocks are code (default).

Preprocessor for Org mode documents.

Blanks the non-code parts of a given file, preserving positions of characters corresponding to code. This way, there is a direct correspondence between source positions and positions in the processed result.

Type of a literate preprocessor: Invariants:

f : Processor

proposition> f pos s /= []

proposition> f pos s >>= layerContent == s

A list of contiguous layers.

A sequence of characters in a file playing the same role.

Role of a character in the file.

Returns True if the role corresponds to Agda code.

Returns True if the layer contains Agda code.