[Agda] Prop was removed in 2.2.8

[Ulf Norell]

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

> Hi, list!
>
> What was the semantics of Prop in versions prior to 2.2.8? (release note
> states it was removed). Was it impredicative as in Coq? What was the reason
> for it to be removed?
>

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.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110825/7a74b7dc/attachment.html