\documentclass{article} \usepackage{agda} \begin{document} \begin{code} module InfixDeclaration where infix 5 _>>_ _<<_ data _>>_ : Set where data _<<_ : Set where \end{code} Let's try some infix declaration with surrounding text. \begin{code} module SurroundingText where \end{code} In the following, we declare the fixity of two operators. \begin{code} infix 5 _+_ _*_ \end{code} A fixity declaration can preceed the actual declaration of the names. \begin{code} postulate _+_ _*_ : Set \end{code} \end{document}