The Coq mailing list

[Groleo Marius <groleo AT gmail.com>]

On Wed, Jan 13, 2010 at 7:11 PM, Adam Chlipala 
<adamc AT hcoop.net>
 wrote:
> Groleo Marius wrote:
>>
>> Fixpoint loop ( woff roff :Z )(n:Z) :=
>>   match n with
>>   | 0 =>  0
>>   | n' =>  loop 1 1 (Zminus n' 1)
>>   end.
>>
>> Error: Cannot guess decreasing argument of fix.
>>
>> Can you point me please to some documents regarding this construct ?
>>
>
> I think [Fixpoint] is well enough documented in the Coq manual, but there is
> a fundamental problem with your definition.  Coq will only accept
> terminating programs, and your function loops forever when [n] is negative.
>
Indeed, Fixpoint is well documented in Coq'Art too; my problem wasn't
Fixpoint itself,
but as I said, the whole construct. I wasn't able to find other
examples of using other types than nat;
I tried using the same pattern as in nat, using the succesor
constructor for Z, Zsucc,
but it didn't worked, neither the Zpos,Zneg.


-- 
Regards, Groleo!