agda/test/LaTeXAndHTML/succeed/Issue2733-2.lagda.tex

\documentclass{article}

\usepackage{agda}

\begin{document}

\begin{AgdaAlign}
\begin{code}
module Issue2733-2 where
\end{code}

Indentation should be inserted before \AgdaKeyword{postulate}, but not
before the last occurrence of \AgdaPrimitiveType{Set}, which should be
aligned with the penultimate occurrence of \AgdaPrimitiveType{Set}:
\begin{code}
  postulate
    A  : Set
    B  : Set →
         Set
\end{code}
\end{AgdaAlign}

\end{document}