Library Beroal.Ackermann
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.
| 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