agda/test/LaTeXAndHTML/succeed/Grapheme-clusters.quick.tex

\documentclass{article}

\usepackage{agda}

\begin{document}

\AgdaPostulate{A} and \AgdaPostulate{B} should be aligned:
\begin{code}%
%
\>[2]\AgdaKeyword{postulate}\<%
\\
\>[2][@{}l@{\AgdaIndent{0}}]%
\>[4]\AgdaPostulate{+̲+̲+̲+̲+̲+̲}%
\>[12]\AgdaPostulate{A}\<%
\\
%
\>[12]\AgdaPostulate{B}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\end{code}

The two \AgdaKeyword{field} keywords should not be aligned:
\begin{code}%
%
\>[2]\AgdaKeyword{record}\AgdaSpace{}%
\AgdaRecord{+̲}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set₁}\AgdaSpace{}%
\AgdaKeyword{where}%
\>[25]\AgdaKeyword{field}\AgdaSpace{}%
\AgdaField{C}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\\
\>[25][@{}l@{\AgdaIndent{0}}]%
\>[26]\AgdaKeyword{field}\AgdaSpace{}%
\AgdaField{D}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\end{code}

\end{document}