The Coq mailing list

[Victor Porton <porton AT narod.ru>]

14.11.2011, 19:17, "Adam Chlipala" 
<adamc AT csail.mit.edu>:
> I'm surprised that [C2] has type [C], so I think Victor has a legitimate
> point here. šThe usual section behavior rules imply to me that [C2]
> should be parametrized over [Other].
>
> On the other hand, the specific proposition used for [Other] is
> dangerously close to inconsistent (easily implies [False] for any
> interesting choice of [Q]), so there may be other serious issues in the
> code.

This is not an issue with the code, because the sole purpose of this code is 
to test how Coq works with particular code.

> Victor Porton wrote:
>
>> šSee also this my bug report:
>>
>> šhttp://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2642
>>
>> š14.11.2011, 18:58, "Thomas 
>>Â Braibant"<thomas.braibant AT gmail.com>:
>>> ššš- C2 has type "C"
>>> ššš- whatever the type of ax2, you cannot apply C to it, because "C" is
>>> šššnot a function type.
>>> ššš- it happens that "ax2 C" as type "Q num", but since your whole script
>>> šššdoes not has much sense to me, I cannot assume that it was what you
>>> šššwanted to write.
>>>
>>> šššCheers,
>>> šššthomas
>>>
>>> šššOn Mon, Nov 14, 2011 at 3:41 PM, Victor 
>>>Â Porton<porton AT narod.ru>
>>>  šwrote:
>>>> ššššHypothesis P: nat->Prop.
>>>> ššššHypothesis Q: nat->Prop.
>>>>
>>>> ššššAxiom Eq: forall x:nat, P(x)<->Q(x).
>>>>
>>>> ššššClass C := {
>>>> šššššnum: nat;
>>>> šššššcond: P num
>>>> šššš}.
>>>>
>>>> ššššSection sect.
>>>> šššššHypothesis Other: forall obj:C, Q num.
>>>>
>>>> šššššInstance C2: C := { num:=0 }.
>>>> šššššProof. Admitted.
>>>> ššššEnd sect.
>>>>
>>>> ššššAxiom ax2: forall obj:C, Q num.
>>>>
>>>> ššššDefinition C3 := C2(ax2).

-- 
Victor Porton - http://portonvictor.org