Grapheme-clusters-with-pragma.lagda.tex 501 B

1234567891011121314151617181920212223242526
  1. \documentclass{article}
  2. \usepackage{agda}
  3. % Make sure that cluster counting is activated.
  4. \begin{code}[hide]
  5. {-# OPTIONS --count-clusters #-}
  6. \end{code}
  7. \begin{document}
  8. \AgdaPostulate{A} and \AgdaPostulate{B} should be aligned:
  9. \begin{code}
  10. postulate
  11. +̲+̲+̲+̲+̲+̲ A
  12. B : Set
  13. \end{code}
  14. The two \AgdaKeyword{field} keywords should not be aligned:
  15. \begin{code}
  16. record +̲ : Set₁ where field C : Set
  17. field D : Set
  18. \end{code}
  19. \end{document}