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