coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Length indexed vector 'index'

From: frank maltman <frank.maltman AT googlemail.com>
To: Adam Chlipala <adam AT chlipala.net>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Length indexed vector 'index'
Date: Sun, 15 May 2011 14:02:21 +0000
Domainkey-signature: a=rsa-sha1; c=nofws; d=googlemail.com; s=gamma; h=date:from:to:cc:subject:message-id:in-reply-to:references:x-mailer :mime-version:content-type:content-transfer-encoding; b=DXea4ceOz1du7L9M7U2ZjwfayE/P7wa3qFXDuLsZAQ+grL5lhvBRAJSk8XAV/EpaS1 IR6niPWQW+05uk+iGHtX3eFr5axnS6oQajAnFDq4KftNigmU2UBsz66RhYyMbr08mv2V Mada5ySUrjqMUF7hDzovpG7QLoe0f3rks+DzY=

On Sun, 15 May 2011 09:43:04 -0400
Adam Chlipala
<adam AT chlipala.net>
wrote:

> frank maltman wrote:
> > Having now completed the finite number type with the assistance
> > of this list, I've moved on to attempting to define a length-indexed
> > vector type:
> >
>
> I just want to make sure you're aware that all of these definitions
> (including the one you're struggling with) also appear in "Certified
> Programming with Dependent Types."

Hah! I actually wasn't aware. I've been reading through it, but I've
only got as far as the chapter on subset types, currently. Thanks for
the notice.

[Coq-Club] Length indexed vector 'index', frank maltman
- Re: [Coq-Club] Length indexed vector 'index', Adam Chlipala
  - Re: [Coq-Club] Length indexed vector 'index', frank maltman
    - Message not available
      - Re: [Coq-Club] Length indexed vector 'index', frank maltman
  - Re: [Coq-Club] Length indexed vector 'index', frank maltman
    - Re: [Coq-Club] Length indexed vector 'index', Matthieu Sozeau
    - Re: [Coq-Club] Length indexed vector 'index', Brandon Moore
      - Re: [Coq-Club] Length indexed vector 'index', frank maltman
  - Re: [Coq-Club] Length indexed vector 'index', frank maltman
    - Re: [Coq-Club] Length indexed vector 'index', Adam Chlipala
      - Re: [Coq-Club] Length indexed vector 'index', frank maltman