[Agda] Prop was removed in 2.2.8

[Ulf Norell]

On Thu, Aug 25, 2011 at 3:52 PM, Pavel Perikov <perikov at gmail.com> wrote:

>
> On Aug 25, 2011, at 5:44 PM, Ulf Norell wrote:
>
> >
> > 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.
>
> Thanks! So now the cost for the proof irrelevance was paid and there's no
> need for Prop?


Yes. See the release notes for 2.2.10 [1] and 2.2.8 [2] for how to use
irrelevant functions and definitions.

/ Ulf

[1] http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Version-2-2-10
[2] http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Version-2-2-8
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110825/c70170ee/attachment.html