[Agda] Prop was removed in 2.2.8

Pavel Perikov perikov at gmail.com
Thu Aug 25 15:33:53 CEST 2011


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?

Pavel



More information about the Agda mailing list