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

\documentclass{article}

\usepackage{agda}

\setlength{\AgdaEmptySkip}{\abovedisplayskip}

\begin{document}

\thispagestyle{empty}

Text.
\begin{code}%
%
\>[2]\AgdaKeyword{postulate}\<%
\\
\>[2][@{}l@{\AgdaIndent{0}}]%
\>[4]\AgdaPostulate{A}%
\>[7]\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\\
%
\\[\AgdaEmptyExtraSkip]%
%
\>[4]\AgdaPostulate{B}%
\>[7]\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\end{code}
More text.

\end{document}