(** we can define Ackermann's function in Coq *)
Definition ackermann := fix recm (m : nat) := match m with
| O => S
| S pm => fix recn (n : nat) := match n with
	| O => recm pm 1
	| S pn => recm pm (recn pn)
	end
end.

(** our definition is equivalent to equational definition *)
Section check.
Variable pm n pn : nat.
Check (refl_equal _) :  ackermann 0 n = S n.
Check (refl_equal _) :  ackermann (S pm) 0 = ackermann pm 1.
Check (refl_equal _) :  ackermann (S pm) (S pn)
	= ackermann pm (ackermann (S pm) pn).
End check.