coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Vladimir Voevodsky <vladimir AT ias.edu>
- To: Tom Prince <tom.prince AT ualberta.net>
- Cc: Coq-Club Club <coq-club AT inria.fr>, coqdev AT inria.fr
- Subject: [Coq-Club] Re: [coqdev] messy behavior with universes
- Date: Sat, 16 Apr 2011 08:43:17 -0400
Uhhh-uhh. I see. I got so used working with fixed universes that I forgot
about this behavior. Thanks! V.
On Apr 15, 2011, at 7:24 PM, Tom Prince wrote:
> On 2011-04-15, Vladimir Voevodsky wrote:
>> In the following example:
>>
>> File 1 (ex1.v) :
>>
>> Definition dneg (X:Type) := ((X -> Empty_set) -> Empty_set).
>>
>>
>> File 2 (ex2.v):
>>
>> Require Export ex1.
>> Variable X:Set.
>> Check (dneg X).
>> Check ((X -> Empty_set)-> Empty_set).
>>
>>
>> Coq responds that (dneg X) is in Type while ((X -> Empty_set)-> Empty_set)
>> is in Set. This does not look right.
>
> This is expected. Everything in Set is also in type, so
>
> Check ((X -> Empty_set)-> Empty_set) : Type.
>
> Unfortunately, coq doesn't currently support looking through the
> definition of dneg to see that (dneg X) is convertible with a term of
> sort Set.
>
> There is limited support for doing this with paramaters of inductives,
> but nothing else.
>
> Tom
- Re: [Coq-Club] Guard Condition, (continued)
- Re: [Coq-Club] Guard Condition,
Gert Smolka
- RE: [Coq-Club] Guard Condition,
Georges Gonthier
- [Coq-Club] Impredicative [ Set ],
Vladimir Voevodsky
- Re: [Coq-Club] Impredicative [ Set ],
Gregory Malecha
- Message not available
- Message not available
- Re: [Coq-Club] Impredicative [ Set ], Vladimir Voevodsky
- Re: [Coq-Club] Impredicative [ Set ], Gregory Malecha
- Re: [Coq-Club] Impredicative [ Set ], Vladimir Voevodsky
- Re: [Coq-Club] Impredicative [ Set ], Pierre Courtieu
- Message not available
- [Coq-Club] messy behavior with universes, Vladimir Voevodsky
- [Coq-Club] Re: [coqdev] messy behavior with universes, Tom Prince
- [Coq-Club] Re: [coqdev] messy behavior with universes, Vladimir Voevodsky
- Re: [Coq-Club] Re: [coqdev] messy behavior with universes, Carlos Simpson
- Re: [Coq-Club] Re: [coqdev] messy behavior with universes, Vladimir Voevodsky
- Message not available
- Re: [Coq-Club] Re: [coqdev] messy behavior with universes, Enrico Tassi
- Re: [Coq-Club] Impredicative [ Set ],
Gregory Malecha
- Message not available
- Re: [Coq-Club] Re: [coqdev] messy behavior with universes, Andreas Abel
- [Coq-Club] THedu'11 at CADE: last call for ext.abstracts, Laurent Théry
- [Coq-Club] Impredicative [ Set ],
Vladimir Voevodsky
- RE: [Coq-Club] Guard Condition,
Georges Gonthier
- Re: [Coq-Club] Guard Condition,
Gert Smolka
- [Coq-Club] an issue with notations, Vladimir Voevodsky
- [Coq-Club] a problem with canonical structures, Vladimir Voevodsky
- Re: [Coq-Club] a problem with canonical structures, Cyril Cohen
- [Coq-Club] Another question, Vladimir Voevodsky
- Re: [Coq-Club] Another question, Vincent Siles
Archive powered by MhonArc 2.6.16.