Ssreflect Users Discussion List

[Christian Doczkal <>]

Thanks for the quick reply. This then immediately leads to my next question: 
Under which conditions/circumstances are the arguments compared left to right 
and under which conditions right to left? 

Regards
Christian


On 08.11.2013, at 11:11, Laurent Théry <> wrote:

> On 11/08/2013 11:02 AM, Christian Doczkal wrote:
>> Hello Everyone
>> 
>> I am trying to understand the packaged structures approach in detail and 
>> there are some things I do not yet understand.
>> In the Ssreflect libraries (e.g. fintype.v) packaged classes are defined 
>> with a third anonymous field of type Type.
>> 
>> Structure type : Type := Pack {sort; _ : class_of sort; _ : Type}.
>> 
>> This extra field also appears in [1], but I could not find an explanation 
>> in the paper. In [2] no such field is used.
>> Correct me if I'm wrong, but it also seems that whenever Pack is applied, 
>> the sort argument and the anonymous argument are the same.
>> So I wonder what purpose this field has.
>> 
>> Thanks in advance.
> 
> As class structure can be very large structure, it is just an optimization 
> to help Coq compare/unify structures.
> With this redundancy, we are sure that whatether order (left right - > 
> right left) is used to look at the arguments
> it will always start with the most discriminant one its sort.
>