agda/test/LaTeXAndHTML/succeed/Indenting7.quick.tex

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

\begin{code}%
\>[0]\AgdaKeyword{module}\AgdaSpace{}%
\AgdaModule{Indenting7}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
%
\\[\AgdaEmptyExtraSkip]%
\>[0][@{}l@{\AgdaIndent{0}}]%
\>[2]\AgdaKeyword{module}\AgdaSpace{}%
\AgdaModule{A₁}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
%
\>[2]\AgdaKeyword{module}\AgdaSpace{}%
\AgdaModule{A₂}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
%
\\[\AgdaEmptyExtraSkip]%
\>[2][@{}l@{\AgdaIndent{0}}]%
\>[4]\AgdaKeyword{module}\AgdaSpace{}%
\AgdaModule{B₁}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
%
\>[4]\AgdaKeyword{module}\AgdaSpace{}%
\AgdaModule{B₂}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
%
\\[\AgdaEmptyExtraSkip]%
\>[4][@{}l@{\AgdaIndent{0}}]%
\>[6]\AgdaKeyword{module}\AgdaSpace{}%
\AgdaModule{C₁}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
%
\>[6]\AgdaKeyword{module}\AgdaSpace{}%
\AgdaModule{C₂}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
%
\\[\AgdaEmptyExtraSkip]%
\>[6][@{}l@{\AgdaIndent{0}}]%
\>[8]\AgdaKeyword{module}\AgdaSpace{}%
\AgdaModule{D₁}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
%
\>[8]\AgdaKeyword{module}\AgdaSpace{}%
\AgdaModule{D₂}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
%
\\[\AgdaEmptyExtraSkip]%
%
\>[6]\AgdaKeyword{module}\AgdaSpace{}%
\AgdaModule{C₃}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
%
\>[6]\AgdaKeyword{module}\AgdaSpace{}%
\AgdaModule{C₄}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
%
\\[\AgdaEmptyExtraSkip]%
%
\>[2]\AgdaKeyword{module}\AgdaSpace{}%
\AgdaModule{A₃}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
\>[2][@{}l@{\AgdaIndent{0}}]%
\>[4]\AgdaKeyword{module}\AgdaSpace{}%
\AgdaModule{B₃}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
\>[4][@{}l@{\AgdaIndent{0}}]%
\>[6]\AgdaKeyword{module}\AgdaSpace{}%
\AgdaModule{C₅}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
\>[6][@{}l@{\AgdaIndent{0}}]%
\>[8]\AgdaKeyword{module}\AgdaSpace{}%
\AgdaModule{D₃}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
%
\>[6]\AgdaKeyword{module}\AgdaSpace{}%
\AgdaModule{C₆}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
%
\>[4]\AgdaKeyword{module}\AgdaSpace{}%
\AgdaModule{B₄}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
%
\>[2]\AgdaKeyword{module}\AgdaSpace{}%
\AgdaModule{A₄}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\end{code}

\end{document}