| 1234567891011121314151617181920212223242526272829303132333435363738394041424344 |
- \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}
|
