coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Equality for inductive type containing list, Klaus Ostermann, 10/06/2016
- Re: [Coq-Club] Equality for inductive type containing list, Dominique Larchey-Wendling, 10/06/2016
- Re: [Coq-Club] Equality for inductive type containing list, Clément Pit--Claudel, 10/06/2016
- Re: [Coq-Club] Equality for inductive type containing list, Klaus Ostermann, 10/06/2016
- Re: [Coq-Club] Equality for inductive type containing list, Dominique Larchey-Wendling, 10/06/2016
- Re: [Coq-Club] Equality for inductive type containing list, Pierre-Marie Pédrot, 10/06/2016
- Re: [Coq-Club] Equality for inductive type containing list, Maxime Dénès, 10/06/2016
- Re: [Coq-Club] Equality for inductive type containing list, Pierre-Marie Pédrot, 10/06/2016
- Re: [Coq-Club] Equality for inductive type containing list, Pierre Courtieu, 10/06/2016
- Re: [Coq-Club] Equality for inductive type containing list, Abhishek Anand, 10/06/2016
- Re: [Coq-Club] Equality for inductive type containing list, Dominique Larchey-Wendling, 10/06/2016
- Re: [Coq-Club] Equality for inductive type containing list, Jonathan Leivent, 10/06/2016
- Re: [Coq-Club] Equality for inductive type containing list, Pierre-Marie Pédrot, 10/06/2016
- Re: [Coq-Club] Equality for inductive type containing list, Pierre-Marie Pédrot, 10/07/2016
- Re: [Coq-Club] Equality for inductive type containing list, Pierre Courtieu, 10/07/2016
- Re: [Coq-Club] Equality for inductive type containing list, Matthieu Sozeau, 10/07/2016
- Re: [Coq-Club] Equality for inductive type containing list, Pierre-Marie Pédrot, 10/07/2016
- Re: [Coq-Club] Equality for inductive type containing list, Pierre-Marie Pédrot, 10/06/2016
- Re: [Coq-Club] Equality for inductive type containing list, Pierre-Marie Pédrot, 10/07/2016
- Re: [Coq-Club] Equality for inductive type containing list, Maxime Dénès, 10/06/2016
- Re: [Coq-Club] Equality for inductive type containing list, Pierre-Marie Pédrot, 10/06/2016
- Re: [Coq-Club] Equality for inductive type containing list, Dominique Larchey-Wendling, 10/06/2016
- Re: [Coq-Club] Equality for inductive type containing list, Dominique Larchey-Wendling, 10/06/2016
Archive powered by MHonArc 2.6.18.