Fixpoint ack (m : nat) : nat -> nat :=
  fix ack_m (n : nat) : nat :=
    match m with
      | 0 => S n
      | S pm =>
        match n with
          | 0 => ack pm 1
          | S pn => ack pm (ack_m pn)
        end
    end.


(*
  Example:
    A(3, 2) = 29
*)

Eval compute in ack 3 2.