agda/test/LaTeXAndHTML/succeed/Issue2474-2.lagda

\documentclass{article}
\usepackage{agda}
\begin{document}

\begin{code}
import Issue2474
\end{code}
\end{document}