coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Strange behaviour of induction with eqn: option

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
Cc: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Strange behaviour of induction with eqn: option
Date: Mon, 28 Oct 2013 08:53:42 +0000
Accept-language: de-DE, en-US

Dear Rui, George, Cedric,

thanks a lot for you answers! They lifted the fog a little bit, but I have to think more around your suggestions to get a clear view. Give me some time to bite through this …

Best regards,

Michael

[Coq-Club] Strange behaviour of induction with eqn: option, michael.soegtrop, 10/24/2013
- Re: [Coq-Club] Strange behaviour of induction with eqn: option, Rui Baptista, 10/24/2013
  - RE: [Coq-Club] Strange behaviour of induction with eqn: option, Soegtrop, Michael, 10/24/2013
    - Re: [Coq-Club] Strange behaviour of induction with eqn: option, Cedric Auger, 10/24/2013
      - Re: [Coq-Club] Strange behaviour of induction with eqn: option, Rui Baptista, 10/25/2013
        
        RE: [Coq-Club] Strange behaviour of induction with eqn: option, Soegtrop, Michael, 10/28/2013
- RE: [Coq-Club] Strange behaviour of induction with eqn: option, Georges Gonthier, 10/24/2013