agda/test/LaTeXAndHTML/succeed/Relative-indentation.quick.tex

\documentclass{article}

\usepackage{agda}

\begin{document}

\begin{code}%
\>[0]\AgdaKeyword{postulate}\<%
\\
\>[0][@{}l@{\AgdaIndent{0}}]%
\>[2]\AgdaPostulate{A}%
\>[5]\AgdaPostulate{B}\<%
\\
\>[5][@{}l@{\AgdaIndent{0}}]%
\>[6]\AgdaPostulate{C}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\end{code}

\begin{code}%
\>[0]\AgdaKeyword{postulate}\<%
\\
\>[0][@{}l@{\AgdaIndent{0}}]%
\>[2]\AgdaPostulate{D}%
\>[5]\AgdaPostulate{E}\<%
\\
%
\\[\AgdaEmptyExtraSkip]%
\>[5][@{}l@{\AgdaIndent{0}}]%
\>[6]\AgdaPostulate{F}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\end{code}

\begin{code}%
\>[0]\AgdaKeyword{postulate}\<%
\\
\>[0][@{}l@{\AgdaIndent{0}}]%
\>[2]\AgdaPostulate{G}%
\>[5]\AgdaPostulate{H}%
\>[8]\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\\
%
\>[2]\AgdaPostulate{I}\<%
\\
\>[2][@{}l@{\AgdaIndent{0}}]%
\>[6]\AgdaPostulate{J}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\end{code}

\begin{AgdaMultiCode}
\begin{code}%
\>[0]\AgdaKeyword{postulate}\<%
\\
\>[0][@{}l@{\AgdaIndent{0}}]%
\>[2]\AgdaPostulate{K}%
\>[5]\AgdaPostulate{L}\<%
\end{code}
\begin{code}%
\>[5][@{}l@{\AgdaIndent{1}}]%
\>[6]\AgdaPostulate{M}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\end{code}
\end{AgdaMultiCode}

\begin{code}%
\>[0]\AgdaKeyword{record}\AgdaSpace{}%
\AgdaRecord{R}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set₁}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
\>[0][@{}l@{\AgdaIndent{0}}]%
\>[2]\AgdaKeyword{field}\AgdaSpace{}%
\AgdaField{N}%
\>[14I]\AgdaSymbol{:}\<%
\\
\>[14I][@{}l@{\AgdaIndent{0}}]%
\>[12]\AgdaPrimitive{Set}\<%
\end{code}

% There is (and should be) trailing whitespace at the end of some
% lines below.

\begin{AgdaAlign}
text \begin{code}        %
\>[0]\AgdaKeyword{module}\AgdaSpace{}%
\AgdaModule{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\end{code} more text
    also text  \begin{code}%
\>[0][@{}l@{\AgdaIndent{1}}]%
\>[4]\AgdaKeyword{postulate}\AgdaSpace{}%
\AgdaPostulate{O}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\end{code} text again

 text          \begin{code}            %
%
\>[4]\AgdaKeyword{postulate}\AgdaSpace{}%
\AgdaPostulate{o}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPostulate{O}\<%
\end{code}   text             
\end{AgdaAlign}

\begin{code}%
\>[0]\AgdaKeyword{postulate}\<%
\\
\>[0][@{}l@{\AgdaIndent{0}}]%
\>[1]\AgdaPostulate{P}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\end{code}

\begin{code}%
\>[0]\AgdaKeyword{module}\AgdaSpace{}%
\AgdaModule{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
\>[0][@{}l@{\AgdaIndent{0}}]%
\>[1]\AgdaKeyword{postulate}\<%
\\
\>[1][@{}l@{\AgdaIndent{0}}]%
\>[2]\AgdaPostulate{Q}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\end{code}

\begin{code}%
\>[0]\AgdaKeyword{module}\AgdaSpace{}%
\AgdaModule{\AgdaUnderscore{}}%
\>[30I]\AgdaKeyword{where}\<%
\\
\>[.][@{}l@{}]\<[30I]%
\>[9]\AgdaKeyword{postulate}\<%
\\
\>[9][@{}l@{\AgdaIndent{0}}]%
\>[10]\AgdaPostulate{S}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\end{code}

\begin{AgdaMultiCode}
\begin{code}%
\>[0]\AgdaKeyword{module}\AgdaSpace{}%
\AgdaModule{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\end{code}
\begin{code}%
\>[0][@{}l@{\AgdaIndent{1}}]%
\>[2]\AgdaKeyword{postulate}%
\>[35I]\AgdaPostulate{T}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\\
\>[.][@{}l@{}]\<[35I]%
\>[12]\AgdaPostulate{U}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\end{code}
\end{AgdaMultiCode}

\begin{AgdaSuppressSpace}
\begin{code}%
\>[0]\AgdaKeyword{module}\AgdaSpace{}%
\AgdaModule{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\end{code}
\begin{code}%
\>[0][@{}l@{\AgdaIndent{1}}]%
\>[2]\AgdaKeyword{postulate}%
\>[42I]\AgdaPostulate{V}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\\
\>[.][@{}l@{}]\<[42I]%
\>[12]\AgdaPostulate{W}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\end{code}
\end{AgdaSuppressSpace}

\begin{code}%
\>[0]\AgdaFunction{X}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set₁}\<%
\\
\>[0]\AgdaFunction{X}%
\>[49I]\AgdaSymbol{=}\<%
\\
\>[.][@{}l@{}]\<[49I]%
\>[2]\AgdaPrimitive{Set}\<%
\end{code}

\begin{code}%
\>[0]\AgdaFunction{Y}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set₁}\<%
\\
\>[0]\AgdaFunction{Y}\AgdaSpace{}%
\AgdaSymbol{=}%
\>[10]\AgdaPrimitive{Set}\<%
\\
%
\\[\AgdaEmptyExtraSkip]%
\>[0]\AgdaFunction{Zzzzzzzzz}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\\
\>[0]\AgdaFunction{Zzzzzzzzz}%
\>[57I]\AgdaBound{X}\<%
\\
\>[.][@{}l@{}]\<[57I]%
\>[10]\AgdaSymbol{=}\AgdaSpace{}%
\AgdaBound{X}\<%
\end{code}

\end{document}