coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] blocked in an elementary proof

From: Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] blocked in an elementary proof
Date: Mon, 13 Dec 2010 02:03:31 +0100

Hi,

On Sun, Dec 12, 2010 at 07:32:55PM +0100, St�phane Lescuyer wrote:

> Following up on Martijn and Petar's replys, I think one way to look at
> this is the following: it is commonly cumbersome to work directly with
> tail-recursive definitions, [...]

Interesting to know! Thanks for your explanation. It helped!

--
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/

[Coq-Club] blocked in an elementary proof, Daniel de Rauglaudre
- Re: [Coq-Club] blocked in an elementary proof, Petar Maksimovic
- Re: [Coq-Club] blocked in an elementary proof, Martijn Vermaat
  - Re: [Coq-Club] blocked in an elementary proof, St�phane Lescuyer
  - Message not available
    - Re: [Coq-Club] blocked in an elementary proof, Daniel de Rauglaudre
- Message not available
  - Re: [Coq-Club] blocked in an elementary proof, Daniel de Rauglaudre
- Message not available
  - Re: [Coq-Club] unblocked, thanks!, Daniel de Rauglaudre
    - Re: [Coq-Club] unblocked, thanks!, Jean-Francois Monin
    - Message not available
      - Re: [Coq-Club] unblocked, thanks!, Daniel de Rauglaudre
        
        Re: [Coq-Club] unblocked, thanks!, Jean-Francois Monin
        
        Message not available
        
        Re: [Coq-Club] unblocked, thanks!, Daniel de Rauglaudre
        
        Re: [Coq-Club] unblocked, thanks!, quentin . carbonneaux
        Re: [Coq-Club] unblocked, thanks!, AUGER Cedric