agda/test/LaTeXAndHTML/succeed/InfixDeclaration.tex

\documentclass{article}
\usepackage{agda}

\begin{document}

\begin{code}%
\>[0]\AgdaKeyword{module}\AgdaSpace{}%
\AgdaModule{InfixDeclaration}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
%
\\[\AgdaEmptyExtraSkip]%
\>[0]\AgdaKeyword{infix}\AgdaSpace{}%
\AgdaNumber{5}\AgdaSpace{}%
\AgdaOperator{\AgdaDatatype{\AgdaUnderscore{}>>\AgdaUnderscore{}}}\AgdaSpace{}%
\AgdaOperator{\AgdaDatatype{\AgdaUnderscore{}<<\AgdaUnderscore{}}}\<%
\\
%
\\[\AgdaEmptyExtraSkip]%
\>[0]\AgdaKeyword{data}\AgdaSpace{}%
\AgdaOperator{\AgdaDatatype{\AgdaUnderscore{}>>\AgdaUnderscore{}}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
\>[0]\AgdaKeyword{data}\AgdaSpace{}%
\AgdaOperator{\AgdaDatatype{\AgdaUnderscore{}<<\AgdaUnderscore{}}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
\>[0]\<%
\end{code}

Let's try some infix declaration with surrounding text.

\begin{code}%
\>[0]\AgdaKeyword{module}\AgdaSpace{}%
\AgdaModule{SurroundingText}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
\>[0]\<%
\end{code}

In the following, we declare the fixity of two operators.

\begin{code}%
\>[0][@{}l@{\AgdaIndent{1}}]%
\>[2]\AgdaKeyword{infix}\AgdaSpace{}%
\AgdaNumber{5}\AgdaSpace{}%
\AgdaOperator{\AgdaPostulate{\AgdaUnderscore{}+\AgdaUnderscore{}}}\AgdaSpace{}%
\AgdaOperator{\AgdaPostulate{\AgdaUnderscore{}*\AgdaUnderscore{}}}\<%
\end{code}

A fixity declaration can precede the actual declaration of the names.

\begin{code}%
%
\>[2]\AgdaKeyword{postulate}\AgdaSpace{}%
\AgdaOperator{\AgdaPostulate{\AgdaUnderscore{}+\AgdaUnderscore{}}}\AgdaSpace{}%
\AgdaOperator{\AgdaPostulate{\AgdaUnderscore{}*\AgdaUnderscore{}}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\end{code}

Fixity declarations can also occur when renaming during import.

\begin{code}%
\>[0]\AgdaKeyword{open}\AgdaSpace{}%
\AgdaModule{SurroundingText}\AgdaSpace{}%
\AgdaKeyword{renaming}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaOperator{\AgdaPostulate{\AgdaUnderscore{}+\AgdaUnderscore{}}}\AgdaSpace{}%
\AgdaSymbol{to}\AgdaSpace{}%
\AgdaKeyword{infixl}\AgdaSpace{}%
\AgdaNumber{5}\AgdaSpace{}%
\AgdaOperator{\AgdaPostulate{\AgdaUnderscore{}+\AgdaUnderscore{}}}\AgdaSymbol{;}%
\>[53]\AgdaOperator{\AgdaPostulate{\AgdaUnderscore{}*\AgdaUnderscore{}}}\AgdaSpace{}%
\AgdaSymbol{to}\AgdaSpace{}%
\AgdaKeyword{infixl}\AgdaSpace{}%
\AgdaNumber{10}\AgdaSpace{}%
\AgdaOperator{\AgdaPostulate{\AgdaUnderscore{}\&\AgdaUnderscore{}}}\AgdaSymbol{)}\<%
\end{code}



\end{document}