The Coq mailing list

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

On 07/10/2016 10:25, Matthieu Sozeau wrote:
> Another idea is to use a "default" fold/logical predicate on the 
> inductive, like Forall for lists, avoiding the new predicate.

Yes, but this predicate is not canonical (not even mentionning Type vs.
Prop issues) and it requires defining it beforehand. I'd prefer having a
really self-contained recursor.

> Why do you think induction couldn't work with those eliminators
> though? You might need with (P0:=...)... to specify the predicates
> for nested occurrences in your case but that's handled I think.

Well, I tried to put myself in the head of a newcomer. Induction failed
because it could not find the instance, and even einduction was failing
with a puzzling message ('einduction needs products'). I would at least
expect that einduction generates an evar for the missing predicates...

PMP

Attachment: signature.asc
Description: OpenPGP digital signature