# Literate Agda

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

-- 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}