The Coq mailing list

["Samuel E. Moelius III" <moelius AT cis.udel.edu>]

On Wednesday, August 20, 2008, at 09:23  AM, Adam Chlipala wrote:

> Venanzio Capretta wrote:
> > I agree with you: For the prefix function, it seems that your 
> > recursive implementation of vectors is much nicer that the inductive 
> > one. But is it always preferable.
>
> I don't have a formal argument, but I think it's likely that the 
> recursive version is never any worse than the inductive version, and 
> we have this example where the recursive version seems much easier to 
> work with.

What about in a more general setting?  Does anyone know of an example 
of type family which can be easily expressed/manipulated as an 
inductive definition, but cannot be so easily expressed/manipulated as 
a recursive definition?

Thanks to all who have replied, BTW.

Sam