The Coq mailing list

[Victor Porton <porton AT narod.ru>]

14.11.2011, 21:45, "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?

Oh, I realized. That works only with Instance keyword. Sorry for a stupid 
question.

>> š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

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