agda/test/LaTeXAndHTML/succeed/Trailing-whitespace.lagda.tex

\documentclass{article}

\usepackage{agda}
\AgdaNoSpaceAroundCode{}

\begin{document}

\hrule
\begin{code}
postulate
  
  A : Set  
  B : Set  
\end{code}
\hrule
\begin{code}
  
\end{code}
\hrule
\begin{code}

\end{code}
\hrule
\begin{code}
\end{code}
\hrule
\begin{code}  
  \end{code}
\hrule
  \begin{code}  
\end{code}
\hrule
  \begin{code}  
    \end{code}
\hrule
\begin{code}
module _ where
\end{code}
\begin{code}
  
  postulate
    C : Set
\end{code}
\hrule
\begin{AgdaAlign}
\begin{code}
postulate
  F  : Set → Set
  X  : F  
\end{code}
\begin{code}
          A
\end{code}
\end{AgdaAlign}
\hrule

\end{document}