coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Fixpoint decreasing parameter:help

From: Groleo Marius <groleo AT gmail.com>
To: Adam Koprowski <adam.koprowski AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Fixpoint decreasing parameter:help
Date: Wed, 13 Jan 2010 22:01:58 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type:content-transfer-encoding; b=Co28N7dIrQhrzoPiVbK1syKqSPqvfyOzr4AWxcaJvnhnyZED4uKmqPUDhR3Y1Cc9bj TGbaRyBdSczsJ4autEEJnps3ut/2eXoD9iH/cQgsrymBA/ZLH+bme77+PqMg+oDGsRZI PeowzWGPdhJNfl5+nCGMM6q4tC01At7UUmKsc=

On Wed, Jan 13, 2010 at 7:15 PM, Adam Koprowski
<adam.koprowski AT gmail.com>
wrote:
>> I'm trying to write a recursive function, that would only loop until a
>> given parameter, n, get equal to 1.
>> [...]
>> Can you point me please to some documents regarding this construct ?
>
> Since you want [n] to decrease from some positive value to 0, why not
> making it a natural number [nat] instead? Then writing what you intend
> should go smoothly and Coq will be able to establish that the function is
> terminating.

Thanks, that worked :)

--
Regards, Groleo!

[Coq-Club] Fixpoint decreasing parameter:help, Groleo Marius
- Re: [Coq-Club] Fixpoint decreasing parameter:help, Adam Chlipala
  - Re: [Coq-Club] Fixpoint decreasing parameter:help, Groleo Marius
- Re: [Coq-Club] Fixpoint decreasing parameter:help, Adam Koprowski
  - Re: [Coq-Club] Fixpoint decreasing parameter:help, Groleo Marius