LiterateAgda

See the official user manual for the most up-to-date version of the information on this page.

Agda supports literate files in which everything is by default a comment. Agda code in a literate file must be enclosed in a \begin{code}, \end{code} pair. Literate Agda files have the extension .lagda. There is no support for presenting the code-blocks in different order in the produced text-document and in the produced Agda-code.

Example:

Normal Agda file (Normal.agda)

  -- This is a comment
  module Normal where

    -- More comments

    -- This is also a comment
    id : {A : Set} -> A -> A
    id x = x

Literate Agda file (Literate.lagda)

  This is a comment
  \begin{code}
  module Literate where
  \end{code}

  More comments

  \begin{code}
    -- This is also a comment
    id : {A : Set} -> A -> A
    id x = x
  \end{code}

Literate Agda and Latex

In order to use literate Agda with Latex you define the code-environment and write your comments in Latex. The lhs2TeX-package has now experimental support for Agda.