Agda-2.3.2.2: test/interaction/Literate.lagda

\begin{code}
module Literate where

postulate A : Set
\end{code}

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