coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] My one of the first tries of advanced induction. Please help to find mistake.

From: Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>
To: Rui Baptista <rpgcbaptista AT gmail.com>
Cc: AUGER Cédric <sedrikov AT gmail.com>, "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] My one of the first tries of advanced induction. Please help to find mistake.
Date: Sun, 13 Oct 2013 23:34:50 +0300

You have nice suggestions.

Reason I chose my definition was that I wanted to try some advanced induction with sigma types. I just chose some random idea and tried to realize it.

[Coq-Club] My one of the first tries of advanced induction. Please help to find mistake., Ilmārs Cīrulis, 10/12/2013
- Re: [Coq-Club] My one of the first tries of advanced induction. Please help to find mistake., AUGER Cédric, 10/12/2013
- Re: [Coq-Club] My one of the first tries of advanced induction. Please help to find mistake., AUGER Cédric, 10/13/2013
  - Re: [Coq-Club] My one of the first tries of advanced induction. Please help to find mistake., AUGER Cédric, 10/13/2013
    - Re: [Coq-Club] My one of the first tries of advanced induction. Please help to find mistake., Rui Baptista, 10/13/2013
      - Re: [Coq-Club] My one of the first tries of advanced induction. Please help to find mistake., Ilmārs Cīrulis, 10/13/2013