Ssreflect Users Discussion List

[Christian Doczkal <>]

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.

-- 
Regards
Christian


[1] François Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau: 
Packaging Mathematical Structures. TPHOLs 2009:327-342
[2] Assia Mahboubi, Enrico Tassi: Canonical Structures for the Working Coq 
User. ITP 2013:19-34