The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

So that's the difference I missed.

 

Thank you very much!

On Mon, Feb 1, 2016 at 1:28 PM, Robbert Krebbers <mailinglists AT robbertkrebbers.nl> wrote:

On 02/01/2016 12:16 PM, Ilmārs Cīrulis wrote:

Fixpoint fold_right A B n (f: B → A → A) (a: A) (L: list B n): A :=
   match L with
   | nil _ => a
   | cons x t => f x (fold_right f a t)
   end.

You have to write this function in a slightly different way so as to convince Coq that f remains constant during each recursive call:

  Definition fold_right A B (f: B → A → A) :
      forall n, A -> list B n -> A :=
    fix go n a L :=
    match L with
    | nil _ => a
    | cons x t => f x (go _ a t)
    end.

Now f is no longer an argument of the fix.

List.fold_right is written in this way too.