Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Equality for inductive type containing list

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Equality for inductive type containing list


Chronological Thread 
  • From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Equality for inductive type containing list
  • Date: Thu, 6 Oct 2016 16:48:31 +0200

On 06/10/2016 16:44, Maxime Dénès wrote:
> Aren't we already doing exactly that for mutual inductive types?

No, the principle defined by default on mutual inductive types is
stupid, as it does not recurse on the other types than self. Note that
there is again a problem of canonicity here. What would be the type of
such a principle here? Shall we return pairs? Or shall we define several
principles?

PMP

Attachment: signature.asc
Description: OpenPGP digital signature




Archive powered by MHonArc 2.6.18.

Top of Page