| 123456789101112131415161718192021222324252627282930313233343536373839404142434445 |
- <!DOCTYPE HTML>
- <html><head><meta charset="utf-8"><title>InfixDeclaration</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Background">\documentclass{article}
- \usepackage{agda}
- \begin{document}
- </a><a id="62" class="Markup">\begin{code}</a>
- <a id="75" class="Keyword">module</a> <a id="82" href="InfixDeclaration.html" class="Module">InfixDeclaration</a> <a id="99" class="Keyword">where</a>
- <a id="106" class="Keyword">infix</a> <a id="112" class="Number">5</a> <a id="114" href="InfixDeclaration.html#130" class="Datatype Operator">_>>_</a> <a id="119" href="InfixDeclaration.html#152" class="Datatype Operator">_<<_</a>
- <a id="125" class="Keyword">data</a> <a id="_>>_"></a><a id="130" href="InfixDeclaration.html#130" class="Datatype Operator">_>>_</a> <a id="135" class="Symbol">:</a> <a id="137" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="141" class="Keyword">where</a>
- <a id="147" class="Keyword">data</a> <a id="_<<_"></a><a id="152" href="InfixDeclaration.html#152" class="Datatype Operator">_<<_</a> <a id="157" class="Symbol">:</a> <a id="159" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="163" class="Keyword">where</a>
- <a id="170" class="Markup">\end{code}</a><a id="180" class="Background">
- Let's try some infix declaration with surrounding text.
- </a><a id="239" class="Markup">\begin{code}</a>
- <a id="252" class="Keyword">module</a> <a id="SurroundingText"></a><a id="259" href="InfixDeclaration.html#259" class="Module">SurroundingText</a> <a id="275" class="Keyword">where</a>
- <a id="282" class="Markup">\end{code}</a><a id="292" class="Background">
- In the following, we declare the fixity of two operators.
- </a><a id="353" class="Markup">\begin{code}</a>
- <a id="368" class="Keyword">infix</a> <a id="374" class="Number">5</a> <a id="376" href="InfixDeclaration.html#492" class="Postulate Operator">_+_</a> <a id="380" href="InfixDeclaration.html#496" class="Postulate Operator">_*_</a>
- <a id="384" class="Markup">\end{code}</a><a id="394" class="Background">
- A fixity declaration can precede the actual declaration of the names.
- </a><a id="467" class="Markup">\begin{code}</a>
- <a id="482" class="Keyword">postulate</a> <a id="SurroundingText._+_"></a><a id="492" href="InfixDeclaration.html#492" class="Postulate Operator">_+_</a> <a id="SurroundingText._*_"></a><a id="496" href="InfixDeclaration.html#496" class="Postulate Operator">_*_</a> <a id="500" class="Symbol">:</a> <a id="502" href="Agda.Primitive.html#311" class="Primitive">Set</a>
- <a id="506" class="Markup">\end{code}</a><a id="516" class="Background">
- Fixity declarations can also occur when renaming during import.
- </a><a id="583" class="Markup">\begin{code}</a>
- <a id="596" class="Keyword">open</a> <a id="601" href="InfixDeclaration.html#259" class="Module">SurroundingText</a> <a id="617" class="Keyword">renaming</a> <a id="626" class="Symbol">(</a><a id="627" href="InfixDeclaration.html#492" class="Postulate Operator">_+_</a> <a id="631" class="Symbol">to</a> <a id="634" class="Keyword">infixl</a> <a id="641" class="Number">5</a> <a id="643" class="Postulate Operator">_+_</a><a id="646" class="Symbol">;</a> <a id="649" href="InfixDeclaration.html#496" class="Postulate Operator">_*_</a> <a id="653" class="Symbol">to</a> <a id="656" class="Keyword">infixl</a> <a id="663" class="Number">10</a> <a id="666" class="Postulate Operator">_&_</a><a id="669" class="Symbol">)</a>
- <a id="671" class="Markup">\end{code}</a><a id="681" class="Background">
- \end{document}
- </a></pre></body></html>
|
