The Coq mailing list

[Victor Porton <porton AT narod.ru>]

I am now learning how to create an object of a derived class having an object 
of a base class.

As the first act I decided to play with plain dependent records (not yet with 
type classes).

But that simple script does not work in some mysterious (for me) reason. 
Please explain why it does not verify.

[[[[
Record A := {
  num: nat
}.

Record B := {
  base : A;
  e: num base > 2
}.

Definition A_Sample: A := {| num := 3 |}.

Definition B_Sample: B := {| base := A_Sample |}.
Proof. Admitted.
]]]]

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