<br><div class="gmail_quote">On Thu, Aug 25, 2011 at 3:52 PM, Pavel Perikov <span dir="ltr"><<a href="mailto:perikov@gmail.com">perikov@gmail.com</a>></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>
><br>
> 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't quite work out, so we removed it.<br>
<br>
</div>Thanks! So now the cost for the proof irrelevance was paid and there'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>