The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

On 12/19/18 3:13 PM, Xuanrui Qi wrote:
> Also, Ackermann is not definable in Coq, unless you trick Coq using 
> Program Fixpoint. IIRC it's actually a loophole, but you won't break 
> anything by introducing inconsistency.
You can quite easily define Ackermann in Coq:

Fixpoint ackermann (m : nat) : nat -> nat :=
  fix inner (n : nat) : nat :=
    match m, n with
    | 0, _ => S n
    | S m, 0 => ackermann m 1
    | S m, S n => ackermann m (inner n)
    end.