The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 06/10/2016 16:29, Dominique Larchey-Wendling wrote:
> So I wonder why the nested induction required by the type of trees ty
> is still not guessed when Coq generates induction principles.

As far as I can tell, there is no canonical induction principle
corresponding to nested inductive types (e.g. here ty depends on list
ty). If we agreed on some standard way, depending for instance on the
fold of the underlying structure, we could easily generate such code.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature