\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 precede the actual declaration of the names. \begin{code} postulate _+_ _*_ : Set \end{code} Fixity declarations can also occur when renaming during import. \begin{code} open SurroundingText renaming (_+_ to infixl 5 _+_; _*_ to infixl 10 _&_) \end{code} \end{document}