Grapheme-clusters.lagda.tex 387 B

123456789101112131415161718192021
  1. \documentclass{article}
  2. \usepackage{agda}
  3. \begin{document}
  4. \AgdaPostulate{A} and \AgdaPostulate{B} should be aligned:
  5. \begin{code}
  6. postulate
  7. +̲+̲+̲+̲+̲+̲ A
  8. B : Set
  9. \end{code}
  10. The two \AgdaKeyword{field} keywords should not be aligned:
  11. \begin{code}
  12. record +̲ : Set₁ where field C : Set
  13. field D : Set
  14. \end{code}
  15. \end{document}