agda/test/LaTeXAndHTML/succeed/Issue2401.tex

% The example below is, modulo a small change, due to Andrés
% Sicard-Ramírez.

\documentclass{article}

\usepackage{agda}

\begin{document}

av
\begin{code}%
%
\>[2]\AgdaKeyword{module}\AgdaSpace{}%
\AgdaModule{Issue2401}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
%
\\[\AgdaEmptyExtraSkip]%
\>[2][@{}l@{\AgdaIndent{0}}]%
\>[4]\AgdaKeyword{data}\AgdaSpace{}%
\AgdaDatatype{Bool}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
\>[4][@{}l@{\AgdaIndent{0}}]%
\>[6]\AgdaInductiveConstructor{true}%
\>[12]\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{Bool}\<%
\\
%
\>[6]\AgdaInductiveConstructor{false}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{Bool}\<%
\\
%
\>[6]\AgdaInductiveConstructor{dunno}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{Bool}\<%
\\
%
\>[6]\AgdaInductiveConstructor{aa}%
\>[12]\AgdaSymbol{:}\AgdaSpace{}%
\AgdaComment{\{-\ \textbackslash{}end\{code\}\ -\}}\AgdaSpace{}%
\AgdaDatatype{Bool}\<%
\\
\>[0]\<%
\end{code}
bleh

\end{document}