\begin{code}%
\>\<%
\\
%
\\
\>\AgdaKeyword{module} \AgdaModule{ThreeNewLines} \AgdaKeyword{where}\<%
\\
%
\\
\>\<%
\end{code}
