- <!DOCTYPE HTML>
- <html><head><meta charset="utf-8"><title>Issue2474</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="61" class="Markup">\begin{code}</a>
- <a id="74" class="Symbol">{-#</a> <a id="78" class="Keyword">OPTIONS</a> <a id="86" class="Pragma">--allow-unsolved-metas</a> <a id="109" class="Symbol">#-}</a>
- <a id="114" class="Keyword">postulate</a>
- <a id="F"></a><a id="126" href="Issue2474.html#126" class="Postulate">F</a> <a id="128" class="Symbol">:</a> <a id="130" class="Symbol">{</a><a id="131" href="Issue2474.html#131" class="Bound">_</a> <a id="133" class="Symbol">:</a> <a id="135" href="Agda.Primitive.html#311" class="Primitive">Set</a><a id="138" class="Symbol">}</a> <a id="140" class="Symbol">→</a> <a id="142" href="Agda.Primitive.html#311" class="Primitive">Set</a>
- <a id="A"></a><a id="147" href="Issue2474.html#147" class="Function">A</a> <a id="149" class="Symbol">:</a> <a id="151" href="Agda.Primitive.html#311" class="Primitive">Set</a>
- <a id="155" href="Issue2474.html#147" class="Function">A</a> <a id="157" class="Symbol">=</a> <a id="159" href="Issue2474.html#126" class="UnsolvedMeta Postulate">F</a>
- <a id="161" class="Markup">\end{code}</a><a id="171" class="Background">
- \end{document}
- </a></pre></body></html>
|
