coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Jonathan Leivent <jonikelee AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Equality for inductive type containing list
Date: Thu, 6 Oct 2016 11:42:27 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f177.google.com
Ironport-phdr: 9a23:KhKv0BZlqN+xqXxu6u5WXs//LSx+4OfEezUN459isYplN5qZpsu+bnLW6fgltlLVR4KTs6sC0LuM9fu6EjxQqdbZ6TZZL8wKD0dEwewt3CUeQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2a3IyL0LW5/ISWaAFVjhK8Z6lzJVO4t1b/rM4T1KllLK8tyhLP6l9Fevpbw38gcVCUmRf/68O98bZs9i1Rv7Qq8MsWAvayRLgxUbENVGduCGsy/sC+7RQ=

On 10/06/2016 11:08 AM, Pierre Courtieu wrote:

The default inductive principles for mutual are dumb and I don't
understand why we keep on generating it.

It's one way to get people to read CPDT or Software Foundations ;-)

-- Jonathan

Re: [Coq-Club] Equality for inductive type containing list, (continued)
- 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/07/2016
        Re: [Coq-Club] Equality for inductive type containing list, Dominique Larchey-Wendling, 10/07/2016
    - Re: [Coq-Club] Equality for inductive type containing list, Andrei Popescu, 10/10/2016