Subject: Ssreflect Users Discussion List
List archive
- From: Robbert Krebbers <>
- To: "" <>
- Subject: [ssreflect] Unused Type field in packed classes
- Date: Sun, 21 Feb 2016 18:29:54 +0100
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None ; spf=None ; spf=None
- Ironport-phdr: 9a23:HNKh1xTLG0F5NeyDB10MZ1OnUtpsv+yvbD5Q0YIujvd0So/mwa64bRON2/xhgRfzUJnB7Loc0qyN4/+mBDdLuM7Y+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq8KVPl4D3WLkKZpJbzyI7izp/vEMhoVjLqtjgjDomVBvP9ps+GVzOFiIlAz97MrjtLRq8iBXpu5zv5UYCfayLOwESukSFy88Pm4x6cb3nRzYV06O4GEdWyMXlABJCk7L9luyCozqqCb0sud2xAGfJtezTLYuWD3k7qFxSRauhj1RZBAj92SCsMt6hq9BvFqCvRF1yYPOe8nBMfN/eqLbctcbXnZadtxWXSZMGJ+/dYYFBecbJqBeq9+u9BM1sRKiCFz0V6vUwThSiyqu0A==
Hello list,
In structure declarations like eqType:
Structure type := Pack {sort; _ : class_of sort; _ : Type}.
What is the purpose of the third anonymous field "_ : Type"? Such a field seems to occur in all algebraic structures in the mathcomp hierarchy and also appears in the Zmodule example at page 7 of [1] but does not seem to be explained in that paper.
Best,
Robbert
[1] Francois Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau. Packaging Mathematical Structures. 2009.
- [ssreflect] Unused Type field in packed classes, Robbert Krebbers, 02/21/2016
- Re: [ssreflect] Unused Type field in packed classes, Assia Mahboubi, 02/21/2016
- Re: [ssreflect] Unused Type field in packed classes, Robbert Krebbers, 02/21/2016
- Re: [ssreflect] Unused Type field in packed classes, Assia Mahboubi, 02/21/2016
Archive powered by MHonArc 2.6.18.