Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification


Chronological Thread 
  • From: Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification
  • Date: Thu, 8 Jun 2017 14:42:20 +0200
  • Organization: LORIA

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.




Archive powered by MHonArc 2.6.18.

Top of Page