coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Adam Chlipala <adam AT chlipala.net>
To: frank maltman <frank.maltman AT googlemail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Length indexed vector 'index'
Date: Sun, 15 May 2011 09:43:04 -0400

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."

[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