coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jean-Francois Dufourd <dufourd AT dpt-info.u-strasbg.fr>
- Cc: Coq Club <coq-club AT pauillac.inria.fr>
- Subject: Re: [Coq-Club] Type hierarchy
- Date: Mon, 12 Oct 2009 08:14:24 +0200
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Thus, all this discussion seems to confirm that to define impredicative types in Coq the only means is to work in Set with the option “impredicative-set”.
Thank you very much for the pointers.
Jean-François
- Re: [Coq-Club] what are "levels" in Coq, (continued)
- Re: [Coq-Club] what are "levels" in Coq,
Vladimir Voevodsky
- Re: [Coq-Club] what are "levels" in Coq, Adam Chlipala
- Re: [Coq-Club] what are "levels" in Coq,
Thorsten Altenkirch
- Re: [Coq-Club] what are "levels" in Coq,
Yves Bertot
- Re: [Coq-Club] what are "levels" in Coq, Lionel Elie Mamane
- [Coq-Club] Type hierarchy,
Jean-Francois Dufourd
- Re: [Coq-Club] Type hierarchy, André Hirschowitz
- Re: [Coq-Club] Type hierarchy, Hugo Herbelin
- Re: [Coq-Club] Type hierarchy, Adam Chlipala
- Re: [Coq-Club] Type hierarchy, Hugo Herbelin
- Re: [Coq-Club] Type hierarchy, Jean-Francois Dufourd
- Re: [Coq-Club] what are "levels" in Coq,
Yves Bertot
- [Coq-Club] an inductive types question, Vladimir Voevodsky
- Re: [Coq-Club] an inductive types question, Adam Chlipala
- Re: [Coq-Club] an inductive types question, Vladimir Voevodsky
- Re: [Coq-Club] an inductive types question, Vladimir Voevodsky
- Re: [Coq-Club] an inductive types question, Thorsten Altenkirch
- Re: [Coq-Club] an inductive types question, Vladimir Voevodsky
- Re: [Coq-Club] an inductive types question, Adam Chlipala
- Re: [Coq-Club] what are "levels" in Coq,
Vladimir Voevodsky
- Re: [Coq-Club] an inductive types question, AUGER Cédric
- Re: [Coq-Club] an inductive types question, André Hirschowitz
- Re: [Coq-Club] an inductive types question, AUGER Cédric
Archive powered by MhonArc 2.6.16.