The Coq mailing list

[Victor Porton <porton AT narod.ru>]

14.11.2011, 21:42, "Pierre Courtieu" 
<Pierre.Courtieu AT cnam.fr>:
> 2011/11/14 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 |}.
>
> B_sample has only one field whereas the type B expects two fields. So
> your record is not complete. You should have:

I've read somewhere that if not all fields of a dependent record are given it 
enters into proof mode where the user may fill missing fields.

Why this does not happen now?

> Lemma e_for_3: num A_Sample > 2.
> Proof.
> ššauto.
> Qed.
>
> Program Definition B_Sample: B := {| base := A_Sample; e:= e_for_3 |}.
>
> P.C.
>
>> šProof. Admitted.
>> š]]]]
>>
>> š--
>> šVictor Porton - http://portonvictor.org

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