\begin{code}
module Literate where

postulate A : Set
\end{code}

\begin{code}
postulate a : A
\end{code}