coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- [Coq-Club] Fixpoint "decreasing on 1st argument" notification, raffaello . giulietti, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Gaetan Gilbert, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, raffaello . giulietti, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Beta Ziliani, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, raffaello . giulietti, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Abhishek Anand, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Morrisett, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Beta Ziliani, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, raffaello . giulietti, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Dominique Larchey-Wendling, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Beta Ziliani, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, raffaello . giulietti, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Dominique Larchey-Wendling, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, raffaello . giulietti, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, raffaello . giulietti, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Pierre-Marie Pédrot, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Maxime Dénès, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Maxime Dénès, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Maxime Dénès, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Beta Ziliani, 06/08/2017
- Re: [Coq-Club] Fixpoint "decreasing on 1st argument" notification, Gaetan Gilbert, 06/08/2017
Archive powered by MHonArc 2.6.18.