coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Fixpoint termination issue; why doesn't this simple example go through?

From: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
To: Michiel Helvensteijn <mhelvens AT gmail.com>
Cc: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Fixpoint termination issue; why doesn't this simple example go through?
Date: Sat, 05 Oct 2013 15:57:53 +0200

On 10/05/2013 03:51 PM, Michiel Helvensteijn wrote:

(2) What is the recommended way of solving this? In my search I've
found some descriptions that might be related, but I'd really
appreciate a simple example.

The following alternative definition does through:

Fixpoint my_sum' (l: NatTree) : nat :=
match l with
| leaf n => n
| inner l => fold_right plus 0 (map my_sum' l)
end.
Definition my_sum (l : list NatTree) : nat :=
fold_right plus 0 (map my_sum' l).

[Coq-Club] Fixpoint termination issue; why doesn't this simple example go through?, Michiel Helvensteijn, 10/05/2013
- Re: [Coq-Club] Fixpoint termination issue; why doesn't this simple example go through?, Robbert Krebbers, 10/05/2013
  - Re: [Coq-Club] Fixpoint termination issue; why doesn't this simple example go through?, Pierre Boutillier, 10/05/2013
    - Re: [Coq-Club] Fixpoint termination issue; why doesn't this simple example go through?, Frédéric Blanqui, 10/07/2013
      - Re: [Coq-Club] Fixpoint termination issue; why doesn't this simple example go through?, Pierre Boutillier, 10/07/2013
        
        Re: [Coq-Club] Fixpoint termination issue; why doesn't this simple example go through?, Frédéric Blanqui, 10/08/2013
- Re: [Coq-Club] Fixpoint termination issue; why doesn't this simple example go through?, Frédéric Blanqui, 10/07/2013