- <!DOCTYPE HTML>
- <html><head><meta charset="utf-8"><title>Issue3989</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--warning</a> <a id="23" class="Pragma">ShadowingInTelescope</a> <a id="44" class="Symbol">#-}</a>
- <a id="49" class="Keyword">postulate</a>
- <a id="61" href="Issue3989.html#61" class="Postulate">_</a> <a id="63" class="Symbol">:</a> <a id="65" class="Symbol">(</a><a id="66" href="Issue3989.html#66" class="ShadowingInTelescope Bound">A</a> <a id="68" href="Issue3989.html#68" class="Bound">A</a> <a id="70" class="Symbol">:</a> <a id="72" href="Agda.Primitive.html#311" class="Primitive">Set</a><a id="75" class="Symbol">)</a> <a id="77" class="Symbol">→</a> <a id="79" href="Agda.Primitive.html#311" class="Primitive">Set</a>
- </pre></body></html>
|
