Ssreflect Users Discussion List

[Georges Gonthier <>]

  The Coq kernel compares right-to-left (for reasons no one seems to 
remember). Type inference and unification generally compare left-to-right, 
except on ground terms, for which they call into the kernel comparison code.
  -- Georges

-----Original Message-----
From: Christian Doczkal [] 
Sent: 08 November 2013 10:20
To: 
Subject: Re: [ssreflect] Anonymous "Type" field in packaged classes

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