The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

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.