LiterateAgda

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.

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}