| 12345678910111213141516171819 |
- <!DOCTYPE HTML>
- <html><head><meta charset="utf-8"><title>Indenting5</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="63" class="Markup">\begin{code}</a>
- <a id="76" class="Keyword">record</a> <a id="Sigma"></a><a id="83" href="Indenting5.html#83" class="Record">Sigma</a> <a id="89" class="Symbol">(</a><a id="90" href="Indenting5.html#90" class="Bound">A</a> <a id="92" class="Symbol">:</a> <a id="94" href="Agda.Primitive.html#311" class="Primitive">Set</a><a id="97" class="Symbol">)</a> <a id="99" class="Symbol">(</a><a id="100" href="Indenting5.html#100" class="Bound">B</a> <a id="102" class="Symbol">:</a> <a id="104" href="Indenting5.html#90" class="Bound">A</a> <a id="106" class="Symbol">→</a> <a id="108" href="Agda.Primitive.html#311" class="Primitive">Set</a><a id="111" class="Symbol">)</a> <a id="113" class="Symbol">:</a> <a id="115" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="119" class="Keyword">where</a>
- <a id="127" class="Keyword">constructor</a> <a id="_,_"></a><a id="139" href="Indenting5.html#139" class="InductiveConstructor Operator">_,_</a>
- <a id="145" class="Keyword">field</a>
- <a id="Sigma.proj₁"></a><a id="155" href="Indenting5.html#155" class="Field">proj₁</a> <a id="161" class="Symbol">:</a> <a id="163" href="Indenting5.html#90" class="Bound">A</a>
- <a id="Sigma.proj₂"></a><a id="169" href="Indenting5.html#169" class="Field">proj₂</a> <a id="175" class="Symbol">:</a> <a id="177" href="Indenting5.html#100" class="Bound">B</a> <a id="179" href="Indenting5.html#155" class="Field">proj₁</a>
- <a id="186" class="Keyword">open</a> <a id="191" href="Indenting5.html#83" class="Module">Sigma</a> <a id="197" class="Keyword">public</a>
- <a id="204" class="Markup">\end{code}</a><a id="214" class="Background">
- \end{document}
- </a></pre></body></html>
|
