AccidentalSpacesAfterBeginCode.tex 227 B

1234567891011121314
  1. \documentclass{article}
  2. \usepackage{agda}
  3. \begin{document}
  4. \begin{code} %
  5. \>[0]\AgdaKeyword{module}\AgdaSpace{}%
  6. \AgdaModule{AccidentalSpacesAfterBeginCode}\AgdaSpace{}%
  7. \AgdaKeyword{where}\<%
  8. \end{code}
  9. \end{document}