The Coq mailing list

[Robbert Krebbers <robbertkrebbers AT student.ru.nl>]

Hi,

Brian E. Aydemir wrote:
> I've encountered this problem before [1], and as far as I know, Adam's 
> suggestion is the way to go.  For the sake of concreteness, I've 
> included below code that implements the basic idea.
>
> Cheers,
> Brian
>
> [1] A non-bug report involving lists and a separate inductive type:
>     http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=1751
Thanks for the help, your answers really helped me out!

I just read the bug report you mentioned, but I'm still wondering why it 
isn't allowed. Is it possible to create a 'badly defined' function this 
way? If so I would be interested in an example (which Yves believed 
exists, but wasn't able to show in that thread).

Cheers,

Robbert