agda/test/LaTeXAndHTML/succeed/Less-extra-indentation.quick.tex

\documentclass{article}

\usepackage{agda}

\usepackage{amsmath}
\usepackage{newunicodechar}
\newunicodechar{₁}{\ensuremath{{}_{\text{1}}}}

\pagestyle{empty}

\begin{document}

\noindent Control:
\begin{code}%
%
\>[2]\AgdaFunction{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set₁}\<%
\\
%
\>[2]\AgdaSymbol{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\end{code}

\noindent No extra indentation (alignment):
\begin{code}[hide]%
%
\>[2]\AgdaFunction{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set₁}\<%
\\
%
\>[2]\AgdaSymbol{\AgdaUnderscore{}}%
\>[6I]\AgdaSymbol{=}\<%
\end{code}
\begin{code}%
\>[.][@{}l@{}]\<[6I]%
\>[4]\AgdaPrimitive{Set}\<%
\end{code}

\noindent No extra indentation (indentation):
\begin{code}[hide]%
%
\>[2]\AgdaFunction{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set₁}\<%
\\
%
\>[2]\AgdaSymbol{\AgdaUnderscore{}}%
\>[9I]\AgdaSymbol{=}\<%
\end{code}
\begin{code}%
\>[9I][@{}l@{\AgdaIndent{1}}]%
\>[5]\AgdaPrimitive{Set}\<%
\end{code}

\noindent No extra indentation (alignment):
\begin{code}[hide]%
%
\>[2]\AgdaKeyword{postulate}\<%
\\
\>[2][@{}l@{\AgdaIndent{0}}]%
\>[4]\AgdaPostulate{\AgdaUnderscore{}}%
\>[10I]\AgdaSymbol{:}\<%
\end{code}
\begin{code}%
\>[.][@{}l@{}]\<[10I]%
\>[6]\AgdaPrimitive{Set}\<%
\end{code}

\noindent No extra indentation (indentation):
\begin{code}[hide]%
%
\>[2]\AgdaKeyword{postulate}\<%
\\
\>[2][@{}l@{\AgdaIndent{0}}]%
\>[4]\AgdaPostulate{\AgdaUnderscore{}}%
\>[11I]\AgdaSymbol{:}\<%
\end{code}
\begin{code}%
\>[11I][@{}l@{\AgdaIndent{1}}]%
\>[7]\AgdaPrimitive{Set}\<%
\end{code}

\noindent No extra indentation (alignment, \texttt{AgdaMultiCode}):
\begin{AgdaMultiCode}
\begin{code}[hide]%
%
\>[2]\AgdaFunction{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set₁}\<%
\\
%
\>[2]\AgdaSymbol{\AgdaUnderscore{}}%
\>[14I]\AgdaSymbol{=}\<%
\end{code}
\begin{code}%
\>[.][@{}l@{}]\<[14I]%
\>[4]\AgdaPrimitive{Set}\<%
\end{code}
\begin{code}[hide]%
%
\>[2]\AgdaFunction{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set₁}\<%
\\
%
\>[2]\AgdaSymbol{\AgdaUnderscore{}}%
\>[17I]\AgdaSymbol{=}\<%
\end{code}
\begin{code}%
\>[.][@{}l@{}]\<[17I]%
\>[4]\AgdaPrimitive{Set}\<%
\end{code}
\end{AgdaMultiCode}

\noindent Extra indentation (indentation, \texttt{AgdaMultiCode}):
\begin{AgdaMultiCode}
\begin{code}[hide]%
%
\>[2]\AgdaFunction{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set₁}\<%
\\
%
\>[2]\AgdaSymbol{\AgdaUnderscore{}}%
\>[20I]\AgdaSymbol{=}\<%
\end{code}
\begin{code}%
\>[20I][@{}l@{\AgdaIndent{1}}]%
\>[5]\AgdaPrimitive{Set}\<%
\end{code}
\begin{code}[hide]%
%
\>[2]\AgdaFunction{\AgdaUnderscore{}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set₁}\<%
\\
%
\>[2]\AgdaSymbol{\AgdaUnderscore{}}%
\>[23I]\AgdaSymbol{=}\<%
\end{code}
\begin{code}%
\>[23I][@{}l@{\AgdaIndent{1}}]%
\>[5]\AgdaPrimitive{Set}\<%
\end{code}
\end{AgdaMultiCode}

\noindent No extra indentation (alignment, \texttt{AgdaMultiCode}):
\begin{AgdaMultiCode}
\begin{code}[hide]%
%
\>[2]\AgdaKeyword{postulate}\<%
\\
\>[2][@{}l@{\AgdaIndent{0}}]%
\>[4]\AgdaPostulate{\AgdaUnderscore{}}%
\>[24I]\AgdaSymbol{:}\<%
\end{code}
\begin{code}%
\>[.][@{}l@{}]\<[24I]%
\>[6]\AgdaPrimitive{Set}\<%
\end{code}
\begin{code}[hide]%
%
\>[2]\AgdaKeyword{postulate}\<%
\\
\>[2][@{}l@{\AgdaIndent{0}}]%
\>[4]\AgdaPostulate{\AgdaUnderscore{}}%
\>[25I]\AgdaSymbol{:}\<%
\end{code}
\begin{code}%
\>[.][@{}l@{}]\<[25I]%
\>[6]\AgdaPrimitive{Set}\<%
\end{code}
\end{AgdaMultiCode}

\noindent Extra indentation (indentation, \texttt{AgdaMultiCode}):
\begin{AgdaMultiCode}
\begin{code}[hide]%
%
\>[2]\AgdaKeyword{postulate}\<%
\\
\>[2][@{}l@{\AgdaIndent{0}}]%
\>[4]\AgdaPostulate{\AgdaUnderscore{}}%
\>[26I]\AgdaSymbol{:}\<%
\end{code}
\begin{code}%
\>[26I][@{}l@{\AgdaIndent{1}}]%
\>[7]\AgdaPrimitive{Set}\<%
\end{code}
\begin{code}[hide]%
%
\>[2]\AgdaKeyword{postulate}\<%
\\
\>[2][@{}l@{\AgdaIndent{0}}]%
\>[4]\AgdaPostulate{\AgdaUnderscore{}}%
\>[27I]\AgdaSymbol{:}\<%
\end{code}
\begin{code}%
\>[27I][@{}l@{\AgdaIndent{1}}]%
\>[7]\AgdaPrimitive{Set}\<%
\end{code}
\end{AgdaMultiCode}

\noindent Extra indentation (indentation, \texttt{AgdaMultiCode}):
\begin{AgdaMultiCode}
\begin{code}[hide]%
%
\>[2]\AgdaKeyword{postulate}\<%
\\
\>[2][@{}l@{\AgdaIndent{0}}]%
\>[4]\AgdaPostulate{Aaa}\AgdaSpace{}%
\AgdaSymbol{:}\<%
\end{code}
\begin{code}%
\>[4][@{}l@{\AgdaIndent{1}}]%
\>[6]\AgdaPrimitive{Set}\<%
\end{code}
\begin{code}[hide]%
%
\>[2]\AgdaKeyword{postulate}\<%
\\
\>[2][@{}l@{\AgdaIndent{0}}]%
\>[4]\AgdaPostulate{Bbb}\AgdaSpace{}%
\AgdaSymbol{:}\<%
\end{code}
\begin{code}%
\>[4][@{}l@{\AgdaIndent{1}}]%
\>[6]\AgdaPrimitive{Set}\<%
\end{code}
\end{AgdaMultiCode}

\end{document}