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

\documentclass{article}

\usepackage{agda}

\begin{document}

\noindent Before.
\begin{AgdaMultiCode}
\begin{code}[hide]%
%
\>[2]\AgdaKeyword{postulate}\<%
\end{code}
\begin{code}%
\>[2][@{}l@{\AgdaIndent{1}}]%
\>[4]\AgdaPostulate{A}%
\>[9]\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\end{code}
\begin{code}%
%
\>[4]\AgdaPostulate{BBB}%
\>[9]\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\end{code}
\end{AgdaMultiCode}
After.

\noindent Before.
\begin{AgdaAlign}
\begin{code}%
%
\>[2]\AgdaKeyword{postulate}\<%
\\
\>[2][@{}l@{\AgdaIndent{0}}]%
\>[4]\AgdaPostulate{C}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\end{code}
\begin{code}[hide]%
%
\>[4]\AgdaPostulate{D}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\end{code}
\begin{code}%
%
\>[4]\AgdaPostulate{E}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\end{code}
\end{AgdaAlign}
After.

\noindent Before.
\begin{AgdaAlign}
\begin{code}%
%
\>[2]\AgdaKeyword{postulate}\<%
\\
\>[2][@{}l@{\AgdaIndent{0}}]%
\>[4]\AgdaPostulate{F}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\end{code}
In between.
\begin{AgdaSuppressSpace}
\begin{code}%
%
\>[2]\AgdaKeyword{postulate}\<%
\\
\>[2][@{}l@{\AgdaIndent{0}}]%
\>[4]\AgdaPostulate{G}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\end{code}
\begin{code}[hide]%
%
\>[2]\AgdaKeyword{postulate}\<%
\end{code}
\begin{code}%
\>[2][@{}l@{\AgdaIndent{1}}]%
\>[4]\AgdaPostulate{H}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\end{code}
\end{AgdaSuppressSpace}
\end{AgdaAlign}
After.

\noindent Before.
\begin{AgdaMultiCode}
\begin{code}%
%
\>[2]\AgdaKeyword{postulate}\<%
\\
\>[2][@{}l@{\AgdaIndent{0}}]%
\>[4]\AgdaOperator{\AgdaPostulate{!\AgdaUnderscore{}!}}%
\>[11]\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\end{code}
\begin{code}[hide]%
%
\>[2]\AgdaKeyword{postulate}\<%
\end{code}
\begin{code}%
\>[2][@{}l@{\AgdaIndent{1}}]%
\>[4]\AgdaOperator{\AgdaPostulate{<!\AgdaUnderscore{}!>}}%
\>[11]\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\end{code}
\end{AgdaMultiCode}
After.

\end{document}