coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Parametricity

From: David Baelde <david.baelde AT gmail.com>
To: Peter LeFanu Lumsdaine <p.l.lumsdaine AT gmail.com>
Cc: Adam Chlipala <adam AT chlipala.net>, Daniel Schepler <dschepler AT gmail.com>, coq-club AT inria.fr
Subject: Re: [Coq-Club] Parametricity
Date: Wed, 30 Mar 2011 21:38:27 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:reply-to:in-reply-to:references:date:message-id :subject:from:to:cc:content-type; b=ZXDR5ED9KqmqW5RXaSoQmN/zXEaLN9pMC7iy5gHhrrLPNqJ7N1T2Iv6DjaD39fteXY ufuQn8Q5ZojG6f3UFqd0ryaEtjOkat1owtGzXw2beu0bzgGCwSxwtirP/bgXlrYTHta5 5fnKLyK6/3por/ILsB5bO9XBoXLwnoWhSajmg=

Hi,

Indeed classic_dec is a clear answer, it's definitely one way to
"analyse" the type.

Thanks everybody for the answers. My first post to the list was pretty
successful.

Cheers,

David

[Coq-Club] Parametricity, David Baelde
- Re: [Coq-Club] Parametricity, Daniel Schepler
  - Re: [Coq-Club] Parametricity, Adam Chlipala
    - Message not available
      - Fwd: [Coq-Club] Parametricity, Daniel Schepler
    - Re: [Coq-Club] Parametricity, Peter LeFanu Lumsdaine
      - Re: [Coq-Club] Parametricity, David Baelde