The Coq mailing list

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

On Tue, Nov 8, 2011 at 5:50 PM, Victor Porton 
<porton AT narod.ru>
 wrote:
> (*
> What's wrong with the following .v file which does not verify:
> How to correct it?
> *)
>
> Class C := {
> šnum: nat;
> šcond: num=0
> }.
>
> Instance C2: C := { num:=0 }.
When I reach this point, I have to prove "0 = 0". Do you really have
difficulties proving "0 = 0"? Maybe Type Classes should wait.

<<<
Proof. reflexivity. Qed.
>>>

> proof.
> šhave (num C2=0) using tauto.
> end proof.
>
>
> --
> Victor Porton - http://portonvictor.org
>