coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Transitivity for a non-standard subtyping relation

From: Adam Chlipala <adamc AT hcoop.net>
To: Nikhil Swamy <nswamy AT microsoft.com>
Cc: "coq-club AT pauillac.inria.fr" <coq-club AT pauillac.inria.fr>
Subject: Re: [Coq-Club] Transitivity for a non-standard subtyping relation
Date: Sat, 13 Jun 2009 08:14:27 -0400
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Do you have a pencil-and-paper proof of this result? I don't have enough intuition about why the theorem is true to be able to make concrete Coq suggestions.

[Coq-Club] Transitivity for a non-standard subtyping relation, Nikhil Swamy
- Re: [Coq-Club] Transitivity for a non-standard subtyping relation, Adam Chlipala
- Re: [Coq-Club] Transitivity for a non-standard subtyping relation, Matthew Brecknell
  - Re: [Coq-Club] Transitivity for a non-standard subtyping relation, Matthew Brecknell
    - RE: [Coq-Club] Transitivity for a non-standard subtyping relation, Nikhil Swamy
      - Re: [Coq-Club] Transitivity for a non-standard subtyping relation, Adam Chlipala
        
        RE: [Coq-Club] Transitivity for a non-standard subtyping relation, Nikhil Swamy
        
        Re: [Coq-Club] Transitivity for a non-standard subtyping relation, Adam Chlipala
        
        RE: [Coq-Club] Transitivity for a non-standard subtyping relation, Nikhil Swamy
        Message not available
        RE: [Coq-Club] Transitivity for a non-standard subtyping relation, Nikhil Swamy
    - [Coq-Club] Module Types, Cedric Auger
      - Re: [Coq-Club] Module Types, Elie Soubiran