The Coq mailing list

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

On 06/10/2016 17:08, Pierre Courtieu wrote:
> The default inductive principles for mutual are dumb and I don't
> understand why we keep on generating it.

Quite true. I know this has been discussed privately between some core
devs at some point, but I don't remember the result. I'd bet on: "this
breaks compatibility"!

> But the ones defined by Scheme...with... . are reasonable. Mimicking
> on nested inductives what Scheme does for mutual would be a very good
> approximation. Won't it?

You're actually right. I'll have a look to check if that is easy to
generate the proper induction this way.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature