coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Heterogenous lists and variable-arity constructors

From: "Roly Perera" <roly.perera AT dynamicaspects.org>
To: "Adam Chlipala" <adamc AT hcoop.net>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Heterogenous lists and variable-arity constructors
Date: Wed, 7 Jan 2009 15:19:10 +0000
Domainkey-signature: a=rsa-sha1; c=nofws; d=googlemail.com; s=gamma; h=message-id:date:from:sender:to:subject:cc:in-reply-to:mime-version :content-type:content-transfer-encoding:content-disposition :references:x-google-sender-auth; b=XUbyUule+gRuzxMBf/Na8RI6MsVoZVHdcLQRQcjCaqP8OUiZKbQ0K3kkP1uOvgjP/i W4CllaZTxm8kWxs7AQGOW76t7Y3V21gSN+RdEh/Ok7LduMpzGLK0/9uXdPugF9FrKwUG a+xyS8i6F2DcAxMuD7BPbmCKh89pmXtrfeZQw=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

2009/1/7 Adam Chlipala
<adamc AT hcoop.net>:

> I expect this is what you're looking for:
>   | App (ls: list type) (c: type): (forall c', fmember _ c' ls -> term c')
> -> term c.

Thanks!  I must have been very close yesterday.  Darn.

> Your original type for [App] doesn't look much like a usual application
> typing rule, in that it omits connections between the types of different
> parts, but I'm assuming that's a conscious simplification that you made.

Indeed.  Thanks again (and the book looks great by the way, looking
forward the final version).

Roly

[Coq-Club] Heterogenous lists and variable-arity constructors, Roly Perera
- Re: [Coq-Club] Heterogenous lists and variable-arity constructors, Adam Chlipala
  - Re: [Coq-Club] Heterogenous lists and variable-arity constructors, Roly Perera
    - Re: [Coq-Club] Heterogenous lists and variable-arity constructors, muad
      - Re: [Coq-Club] Heterogenous lists and variable-arity constructors, Roly Perera