agda/test/LaTeXAndHTML/succeed/ltgt.lagda

\documentclass{article}

\usepackage{agda}

\begin{document}
\begin{code}
module ltgt where

<> : Set _
<> = Set

\end{code}
\end{document}