123456789101112131415161718192021222324 |
- \documentclass{article}
- \usepackage{agda}
- \begin{document}
- \begin{code}%
- \>[0]\AgdaKeyword{module}\AgdaSpace{}%
- \AgdaModule{NoNewLinesVsNewLines}\AgdaSpace{}%
- \AgdaKeyword{where}\<%
- \end{code}
- \begin{code}%
- \>[0]\<%
- \\
- \>[0]\AgdaKeyword{module}\AgdaSpace{}%
- \AgdaModule{Test2}\AgdaSpace{}%
- \AgdaKeyword{where}\<%
- \\
- \>[0]\<%
- \end{code}
- \end{document}
|