The Coq mailing list

[Victor Porton <porton AT narod.ru>]

[[[
Class C := {
  x: nat;
  cond: x = 0
}.

About cond.
]]]

This tells that [cond] is a function which receives an argument of type C.

But what is it meanings? If the argument x is of type C, it is already 
verified that [cond x] is true! No need to verify it second time!

Maybe I misunderstand something, but it seems for me that to make sense we 
need to automatically define C_Base which would be the record without 
conditions:

Class C_Base := {
  x: nat
}.

and then have "cond" to accept arguments of type C_Base, not C.

Please comment on my (mis)understanding on how it should work.

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