The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Le 08/06/2017 à 14:38, 
raffaello.giulietti AT supsi.ch
 a écrit :
> Hello,
> 
> consider the following z function
> 
> Fixpoint z (n: nat): nat := 0 * z n.
> 
> which Coq accepts with the usual notification "decreasing on 1st argument".

I suppose that during type-checking, Coq performs some kind of reduction
and sees that 0 * z n reduces to 0 (definition of mult) ... hence there
is no recursive sub-call.

On the contrary, the following fails

Fixpoint z (n: nat): nat := z n * 0.