The Coq mailing list

[Victor Porton <porton AT narod.ru>]

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).