| 12345678910111213141516171819202122232425 |
- <!DOCTYPE HTML>
- <html><head><meta charset="utf-8"><title>Issue2733-2</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Background">\documentclass{article}
- \usepackage{agda}
- \begin{document}
- \begin{AgdaAlign}
- </a><a id="81" class="Markup">\begin{code}</a>
- <a id="94" class="Keyword">module</a> <a id="101" href="Issue2733-2.html" class="Module">Issue2733-2</a> <a id="113" class="Keyword">where</a>
- <a id="119" class="Markup">\end{code}</a><a id="129" class="Background">
- Indentation should be inserted before \AgdaKeyword{postulate}, but not
- before the last occurrence of \AgdaPrimitiveType{Set}, which should be
- aligned with the penultimate occurrence of \AgdaPrimitiveType{Set}:
- </a><a id="341" class="Markup">\begin{code}</a>
- <a id="356" class="Keyword">postulate</a>
- <a id="A"></a><a id="370" href="Issue2733-2.html#370" class="Postulate">A</a> <a id="373" class="Symbol">:</a> <a id="375" href="Agda.Primitive.html#311" class="Primitive">Set</a>
- <a id="B"></a><a id="383" href="Issue2733-2.html#383" class="Postulate">B</a> <a id="386" class="Symbol">:</a> <a id="388" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="392" class="Symbol">→</a>
- <a id="403" href="Agda.Primitive.html#311" class="Primitive">Set</a>
- <a id="407" class="Markup">\end{code}</a><a id="417" class="Background">
- \end{AgdaAlign}
- \end{document}
- </a></pre></body></html>
|
