The Coq mailing list

[Michiel Helvensteijn <mhelvens AT gmail.com>]

On Fri, Jul 19, 2013 at 7:23 PM, Michiel Helvensteijn
<mhelvens AT gmail.com>
 wrote:

> (1)  Most of what I've tried has been based on Daniel Schepler answer
> to Jacques-Henri. He supplied a custom recursion principle. This lead
> me to believe that perhaps Coq uses `mylist_rect` (or `mylist_rec`) to
> check structural reduction by the `short_lists1` function.
> Jacques-Henri seemed satisfied with the answer (though he mentions a
> drawback). I myself, however, still cannot get his `short_lists1`
> function accepted by Coq. What am I missing?

Sorry, I mixed up my examples here. :-)

I meant to refer to his `test2` function, of course, not my own 
`short_lists1`.

--
www.mhelvens.net