<br><div class="gmail_quote">On Thu, Aug 25, 2011 at 3:52 PM, Pavel Perikov <span dir="ltr">&lt;<a href="mailto:perikov@gmail.com">perikov@gmail.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">

<div class="im"><br>
On Aug 25, 2011, at 5:44 PM, Ulf Norell wrote:<br>
<br>
&gt;<br>
&gt; It was an experimental universe whose inhabitants (if you enabled the flag --proof-irrelevance) were syntactically restricted to have at most one element. The idea was that you could get proof irrelevance for Prop cheaply. It didn&#39;t quite work out, so we removed it.<br>


<br>
</div>Thanks! So now the cost for the proof irrelevance was paid and there&#39;s no need for Prop?</blockquote><div><br></div><div>Yes. See the release notes for 2.2.10 [1] and 2.2.8 [2] for how to use irrelevant functions and definitions.</div>

<div><br></div><div>/ Ulf</div><div><br></div><div>[1] <a href="http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Version-2-2-10">http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Version-2-2-10</a></div><div>[2] <a href="http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Version-2-2-8">http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Version-2-2-8</a></div>

</div>