| 123456789101112131415161718192021222324 |
- <!DOCTYPE HTML>
- <html><head><meta charset="utf-8"><title>Issue2401</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Background">% The example below is, modulo a small change, due to Andrés
- % Sicard-Ramírez.
- \documentclass{article}
- \usepackage{agda}
- \begin{document}
- av
- </a><a id="146" class="Markup">\begin{code}</a>
- <a id="161" class="Keyword">module</a> <a id="168" href="Issue2401.html" class="Module">Issue2401</a> <a id="178" class="Keyword">where</a>
- <a id="189" class="Keyword">data</a> <a id="Bool"></a><a id="194" href="Issue2401.html#194" class="Datatype">Bool</a> <a id="199" class="Symbol">:</a> <a id="201" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="205" class="Keyword">where</a>
- <a id="Bool.true"></a><a id="217" href="Issue2401.html#217" class="InductiveConstructor">true</a> <a id="223" class="Symbol">:</a> <a id="225" href="Issue2401.html#194" class="Datatype">Bool</a>
- <a id="Bool.false"></a><a id="236" href="Issue2401.html#236" class="InductiveConstructor">false</a> <a id="242" class="Symbol">:</a> <a id="244" href="Issue2401.html#194" class="Datatype">Bool</a>
- <a id="Bool.dunno"></a><a id="255" href="Issue2401.html#255" class="InductiveConstructor">dunno</a> <a id="261" class="Symbol">:</a> <a id="263" href="Issue2401.html#194" class="Datatype">Bool</a>
- <a id="Bool.aa"></a><a id="274" href="Issue2401.html#274" class="InductiveConstructor">aa</a> <a id="280" class="Symbol">:</a> <a id="282" class="Comment">{- \end{code} -}</a> <a id="299" href="Issue2401.html#194" class="Datatype">Bool</a>
- <a id="305" class="Markup">\end{code}</a><a id="315" class="Background">
- bleh
- \end{document}</a></pre></body></html>
|
