Require Import Utf8.

Section FOLD.
  Context {A: Type} (f: A → A) (a: A).
  Fixpoint fold (n: nat) : A :=
    match n with
    | O => a
    | S n' => f (fold n')
    end.
End FOLD.

Definition ackermann : nat → nat → nat :=
  fold (λ g, fold g (g (S O))) S.