The Coq mailing list

[Victor Porton <porton AT narod.ru>]

(*
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 }.
proof.
  have (num C2=0) using tauto.
end proof.


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