coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Prefixes of a vector

From: "Samuel E. Moelius III" <moelius AT cis.udel.edu>
To: Adam Chlipala <adamc AT hcoop.net>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Prefixes of a vector
Date: Tue, 19 Aug 2008 17:58:49 -0400
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Adam,

For the meantime, I would like to let my original question stand. But, given how much simpler your solution is, I find it hard to argue with this:

That kind of type family works out much better as a recursive definition than as an inductive definition in Coq.

Thanks!

Sam

[Coq-Club] Prefixes of a vector, Samuel E. Moelius III
- Re: [Coq-Club] Prefixes of a vector, Adam Chlipala
  - Re: [Coq-Club] Prefixes of a vector, Samuel E. Moelius III
    - Re: [Coq-Club] Prefixes of a vector, Pierre Casteran
- Re: [Coq-Club] Prefixes of a vector, Venanzio Capretta
  - Re: [Coq-Club] Prefixes of a vector, Adam Chlipala
    - Re: [Coq-Club] Prefixes of a vector, Venanzio Capretta
      - Re: [Coq-Club] Prefixes of a vector, Adam Chlipala
        
        Re: [Coq-Club] Prefixes of a vector, Samuel E. Moelius III
        
        Re: [Coq-Club] Prefixes of a vector, Adam Chlipala
      - Re: [Coq-Club] Prefixes of a vector, Conor McBride
        
        Re: [Coq-Club] Prefixes of a vector, Matthieu Sozeau