coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Substructures with Type Classes

From: Richard Dapoigny <richard.dapoigny AT univ-savoie.fr>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Substructures with Type Classes
Date: Wed, 29 Jan 2014 22:49:27 +0100

Hi,
we are working on the field declared with :> inType Classes (substructures) but we do not know exactly what are the mathematical properties of this operator (e.g., transitivity, ...). Since we want to reason using that operator, it is crucial to explicit these properties. For instance what happens when we nest substructures?
Thanks.
Patrick & Richard

begin:vcard
fn:Richard Dapoigny
n:Dapoigny;Richard
email;internet:richard.dapoigny AT univ-savoie.fr
tel;work:+33 450 09 65 29
tel;cell:+33 621 35 31 43
version:2.1
end:vcard

[Coq-Club] Substructures with Type Classes, Richard Dapoigny, 01/29/2014