coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adamc AT hcoop.net>
- To: Keiko Nakata <keiko AT kurims.kyoto-u.ac.jp>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] case & inversion, Set & Prop
- Date: Fri, 07 Aug 2009 10:09:14 -0400
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Keiko Nakata wrote:
I hit this problem in an attempt to use Prop as impredicative Set. Having learned that the use of Set-valued nat confused me, I wonder if I can avoid them. Namely, is there a Prop-valued equivalent to nat and Z?
While I can't give you a very formal answer, I can say this, as someone who has spent a lot of time trying to do crafty things with impredicativity: you can rarely if ever switch seamlessly from predicative to impredicative computation. The elimination restrictions really do in practice keep you from doing some common computational things impredicatively.
Perhaps you can give us more background on your application, so that we can give more targeted advice.
- [Coq-Club] case & inversion, Set & Prop, Keiko Nakata
- Re: [Coq-Club] case & inversion, Set & Prop,
Adam Chlipala
- Re: [Coq-Club] case & inversion, Set & Prop,
Keiko Nakata
- Re: [Coq-Club] case & inversion, Set & Prop, Adam Chlipala
- Re: [Coq-Club] case & inversion, Set & Prop,
Keiko Nakata
- Re: [Coq-Club] case & inversion, Set & Prop,
Taral
- Re: [Coq-Club] case & inversion, Set & Prop,
Keiko Nakata
- Re: [Coq-Club] case & inversion, Set & Prop, Adam Chlipala
- Re: [Coq-Club] case & inversion, Set & Prop,
Keiko Nakata
- Re: [Coq-Club] case & inversion, Set & Prop,
Adam Chlipala
- Re: [Coq-Club] case & inversion, Set & Prop,
Keiko Nakata
- Re: [Coq-Club] case & inversion, Set & Prop, Adam Chlipala
- Re: [Coq-Club] case & inversion, Set & Prop,
Keiko Nakata
- Re: [Coq-Club] case & inversion, Set & Prop,
Adam Chlipala
- Re: [Coq-Club] case & inversion, Set & Prop, Keiko Nakata
- Re: [Coq-Club] case & inversion, Set & Prop,
Keiko Nakata
- Re: [Coq-Club] case & inversion, Set & Prop, Adam Chlipala
- Re: [Coq-Club] case & inversion, Set & Prop,
Keiko Nakata
- Re: [Coq-Club] case & inversion, Set & Prop,
Adam Chlipala
Archive powered by MhonArc 2.6.16.