The Coq mailing list

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

I guess we have all understood that you think that Coq should be easy
to understand at first sight and that reading the documentation is
pretty boring, but maybe, juuuuust maybe, you should have a look at
http://coq.inria.fr/refman/Reference-Manual004.html#toc14
and
http://coq.inria.fr/refman/Reference-Manual024.html?
You know, just to have an idea of what records actually are in Coq,
and projectors, and type classes.

Alexandre

On Mon, Nov 7, 2011 at 3:25 PM, Victor Porton 
<porton AT narod.ru>
 wrote:
> [[[
> 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
>