The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

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.