The Coq mailing list

[Victor Porton <porton AT narod.ru>]

08.11.2011, 00:30, "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

I've reread 
http://coq.inria.fr/refman/Reference-Manual004.html#toc14
and
http://coq.inria.fr/refman/Reference-Manual024.html

Alexandre, it seems in turn, that you've read only subject of my email.

There was no answer to my question there.

My question why we would need class condition function defined in such way 
(rudely speaking, taking a class as an argument)?

See below for my exact question.

> 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