The Coq mailing list

[Vincent Siles <vincent.siles AT ens-lyon.org>]

I already explained to you that these classes are not the same the
classes you can find in object oriented programming like Java or C++.

Please learn the difference and stop asking to change Coq to be
like you want because you can't read the manual.



2011/11/14 Victor Porton 
<porton AT narod.ru>:
> Oh, I found a solution myself:
>
> Instance sample: Derived := {
>  link:={|n:=0|}
> }.
> trivial.
>
> But I think, it would be better (for a future version of Coq) if my naive 
> solution (see below) also worked.
>
> 15.11.2011, 00:33, "Victor Porton" 
>Â <porton AT narod.ru>:
>> This does not compile. First: is it a feature or a misfeature? Second: How 
>> to write what I intended in Coq 8.3pl2?
>>
>> [[[[
>> Class Base := {
>>   n: nat
>> }.
>>
>> Class Derived := {
>>   link :> Base
>> }.
>>
>> Instance sample: Derived := {
>>   n := 0
>> }.
>> ]]]]
>>
>> --
>> Victor Porton - http://portonvictor.org
>
> --
> Victor Porton - http://portonvictor.org
>