[Agda] Prop was removed in 2.2.8

Pavel Perikov perikov at gmail.com
Thu Aug 25 15:52:29 CEST 2011


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 need for Prop?

P.




More information about the Agda mailing list