The Coq mailing list

[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