The Coq mailing list

[Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>]

2011/11/8 Victor Porton 
<porton AT narod.ru>:
> The difficulty is not to prove 0 = 0 but with getting the "num" field of 
> the current class instance in the proof of the instance.
>
> If I just remove "have (num C2=0) using tauto" it verifies, but my point is 
> not just to verify the theory but to study how to write proofs of type 
> classes validity.

C2 does not exist yet, you are defining it. So of course you can't use "num 
C2"!

> Well, Alexandre, you are right supposing that my knowledge of tactics is 
> weak. I want to learn more about tactics, but only after I will know how to 
> denote the current instance in an instance proof.

Still.... "0=0" should come first.

Alexandre