coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Wojciech Moczydlowski <wm174746 AT zodiac.mimuw.edu.pl>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] Impredicativity in Coq
- Date: Fri, 25 Jun 2004 21:12:21 +0200 (CEST)
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hello,
I have a question regarding impredicativity in Coq. In System F
and hence in Calculus of Constructions one can build logical operators and
equality
using only universal quantification on Prop. The resulting definitions are
impredicative. The standard library in Coq defines conjuction,
disjunction, existence and equality using only inductive definitions, with
no (apparent) impredicativity present. Moreover, Set is no longer
impredicative in v8.0.
Hence the question - can someone point me where the
impredicativity of Prop is essentially used in the standard library or in
applications?
I.e. I would be happy to see a use of Prop which couldn't be done using Set
and
Type(i) with sum/prod/sigS instead of or/and/exists.
Thanks,
Wojtek
- [Coq-Club] nat : Type?, Wojciech Moczydlowski
- Re: [Coq-Club] nat : Type?,
Pierre Casteran
- [Coq-Club] convertibility,
Jean-Yves Vion-Dury
- Re: [Coq-Club] convertibility, Houda Anoun
- [Coq-Club] Impredicativity in Coq, Wojciech Moczydlowski
- [Coq-Club] convertibility,
Jean-Yves Vion-Dury
- Re: [Coq-Club] nat : Type?,
Pierre Casteran
Archive powered by MhonArc 2.6.16.